Two-round extraction by the actual flip-flop look-ahead

The concrete three-call program has a nearly uniform second output while retaining the transcript, full right state, and both first outputs. The sources factor given the transcript; honest and tampered inputs on either side may be arbitrarily correlated. The hypotheses are average joint source envelopes and the original seed-prefix discrepancy. No supplied extractor or intermediate-seed guarantee is assumed.

The proof instantiates the finite two-round argument of Chattopadhyay--Goyal--Li, Non-Malleable Extractors and Codes, with their Many Tampered Extensions, Lemma 6.5 and Claim 6.6, printed pp.25--28, https://arxiv.org/pdf/1505.00107, with the actual matched-width scheduled programs. It does not yet prove the two-refresh flip-flop invariant or the longer advice-bit iteration. The conservative matched parameters are credited separately in Scheduled.Matched.

theorem Algebraic.Cutwidth.Extractor.flipFlopLookAheadWeight_eq (n L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → Fin n → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) : flipFlopLookAheadWeight n L e w l r x x' q q' = lookAheadExtractionWeight w l r x x' q q' (flipFlopSeedPrefix L) (matchedBlockExtractor n 24 L e) (matchedBlockExtractor (matchedBlockOutputBits 64 L) 24 L e)

The actual program law is precisely the three-call law with the proved matched extractors.

theorem Algebraic.Cutwidth.Extractor.flipFlopLookAheadWeight_probability (n L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → Fin n → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (flipFlopLookAheadWeight n L e w l r x x' q q')

Every normalized conditionally factored source has a normalized actual output law.

theorem Algebraic.Cutwidth.Extractor.flipFlopLookAhead_dist_le (n L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (length : Nat.clog 2 (n + 1) ≤ L) (right_length : Nat.clog 2 (matchedBlockOutputBits 64 L + 1) ≤ L) (room : 64 ≤ L) (error : e + 24 + 2 ≤ L) (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → Fin n → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (μ ν : Z → ℝ) {δ : ℝ} (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (left_nonnegative : ∀ (z : Z), 0 ≤ μ z) (right_nonnegative : ∀ (z : Z), 0 ≤ ν z) (left_cap : ∀ (z : Z) (x₀ : Fin n → Bool), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (right_cap : ∀ (z : Z) (q₀ : Fin (matchedBlockOutputBits 64 L) → Bool), w z * mapWeight (q z) (r z) q₀ ≤ ν z) (seed : weightDist (retainedSeedWeight w r fun (z : Z) (b : B) => flipFlopSeedPrefix L (q z b)) (uniformSecondWeight (retainedSeedWeight w r fun (z : Z) (b : B) => flipFlopSeedPrefix L (q z b))) ≤ δ) : have K := 2 ^ (2 ^ 62 * L); have M := Fintype.card ((Fin (matchedBlockSeedBits L) → Bool) × (Fin (matchedBlockSeedBits L) → Bool)); weightDist (flipFlopLookAheadWeight n L e w l r x x' q q') (uniformSecondWeight (flipFlopLookAheadWeight n L e w l r x x' q q')) ≤ 3 * (2 ^ e)⁻¹ + δ + ↑K * (1 + ↑M) * ∑ z : Z, μ z + ↑K * ↑M * ∑ z : Z, ν z

Actual look-ahead extraction retains the right state and both first outputs.