One complete advice-bit step before advice differs

For arbitrary honest and tampered bits, the actual eight-call program preserves approximate uniformity given both complete look-ahead histories and the full original left state. The current tampered right state may remain arbitrarily correlated with the honest state. Only the honest state's joint discrepancy and original X/Y source envelopes are assumed. The final tampered output is not observed in this law.

Both look-ahead passes and both refreshes use the actual matched-width programs. The first refresh derives the second state's discrepancy; it is not a supplied intermediate invariant. Exact first-history factors account for the displayed average entropy and error losses.

This is the weak continuation needed before the first unequal advice bit in Chattopadhyay--Goyal--Li, Algorithm 2 and Claim 6.11, printed pp.31--32: https://arxiv.org/pdf/1505.00107. The conservative finite error estimate is the deduction formalized here. Advice.Extraction completes the advice-chain induction and its final strong-extraction step (adviceCorrelationBreaker_dist_le).

theorem Algebraic.Cutwidth.Extractor.flipFlopOutput_weak_dist_le (n m L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (guard : FlipFlopSizeGuard n m L e) (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → Fin n → Bool) (y y' : Z → B → Fin m → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (b b' : 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) (y₀ : Fin m → Bool), w z * mapWeight (y z) (r z) y₀ ≤ ξ z) (state : weightDist (retainedSeedWeight w r q) (uniformSecondWeight (retainedSeedWeight w r q)) ≤ ρ) : have K := 2 ^ (2 ^ 62 * L); have J := 2 ^ (2 ^ 142 * L); have D := ↑(Fintype.card (Fin (matchedBlockSeedBits L) → Bool)); have C := ↑(Fintype.card (Fin (matchedBlockOutputBits 64 L) → Bool)); have ε := (2 ^ e)⁻¹; weightDist (flipFlopOutputWeight n m L e w l r x x' y y' q q' b b') (uniformSecondWeight (flipFlopOutputWeight n m L e w l r x x' y y' q q' b b')) ≤ 4 * ρ + 12 * ε + ↑K * (1 + D ^ 2) * (2 + D ^ 4) * ∑ z : Z, μ z + 3 * ↑K * D ^ 2 / C + ↑J * (2 * C ^ 3 + C ^ 5) * ∑ z : Z, ξ z

A complete actual step preserves weak uniformity for any pair of advice bits.