Concrete look-ahead extraction after a nearly uniform refresh

The prefix of a uniform right state is uniform. Together with finite distribution repair, this lets the actual matched-width look-ahead use a nearly uniform right state without a pointwise entropy premise for it. The original right state and both first look-ahead outputs are retained; comparison with their actual marginal charges the refresh error twice.

This is the repair step between passes of the flip-flop argument of Chattopadhyay--Goyal--Li, Non-Malleable Extractors and Codes, with their Many Tampered Extensions, Lemma 6.8: https://arxiv.org/pdf/1505.00107. The theorem instantiates both extractor calls with the actual scheduled programs and gives an explicit finite bound. The complete opposite-advice and iterated correlation-breaking guarantees are proved in Opposite.UniformState and Advice.Extraction (adviceCorrelationBreaker_dist_le).

theorem Algebraic.Cutwidth.Extractor.flipFlopSeedPrefix_uniform (L : ℕ) : mapWeight (flipFlopSeedPrefix L) (uniformWeight (Fin (matchedBlockOutputBits 64 L) → Bool)) = uniformWeight (Fin (matchedBlockSeedBits L) → Bool)

The actual seed-width prefix of a uniform refresh-width state is uniform.

theorem Algebraic.Cutwidth.Extractor.flipFlopLookAhead_uniformState_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)) (nonnegative : ∀ (z : Z), 0 ≤ μ z) (cap : ∀ (z : Z) (x₀ : Fin n → Bool), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (state : weightDist (retainedSeedWeight w r q) (uniformSecondWeight (retainedSeedWeight w r q)) ≤ ρ) : 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)⁻¹ + 2 * ρ + ↑K * (1 + ↑M) * ∑ z : Z, μ z + ↑K * ↑M / ↑(Fintype.card (Fin (matchedBlockOutputBits 64 L) → Bool))

The actual look-ahead needs only joint approximate uniformity of its right state.