The actual honest-false, tampered-true flip-flop guarantee

The output of flipFlopStep on honest advice false is nearly uniform given the complete two-pass transcript, the opposite-advice tampered final output, and the entire original left state. Inputs on either side may be arbitrarily correlated; the original left and right kernels factor given the old transcript. Only original honest source envelopes and the original prefix discrepancy are assumed. Every extractor is the actual scheduled matched-width Boolean program.

The first refresh has error ρ. A correlated repair preserves both original source envelopes and makes that coordinate exactly uniform given the first transcript. The second look-ahead and final refresh then apply to that law. Returning to the actual retained transcript costs 2 * ρ. The first transcript multiplies the total left envelope by M^4 and the right envelope by N^2; the last refresh yields the displayed N^5 term. Cardinalities stay symbolic, with no enumeration of their large Boolean alphabets.

This proves one advice orientation in Chattopadhyay--Goyal--Li's Algorithm 1 and Lemma 6.8, Section 6.3, https://arxiv.org/pdf/1505.00107. The common-scale implementation and this conservative finite accounting are the checked specialization here. The other orientation is proved in Opposite.True. Advice.Extraction proves the complete advice-chain guarantee (adviceCorrelationBreaker_dist_le).

theorem Algebraic.Cutwidth.Extractor.flipFlopOppositeWeight_probability (n m 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) (y y' : Z → B → Fin m → Bool) (q q' : Z → B → Fin (matchedBlockOutputBits 64 L) → Bool) (b : Bool) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (flipFlopOppositeWeight n m L e w l r x x' y y' q q' b)

The direct original-law output is normalized for either honest advice bit.

theorem Algebraic.Cutwidth.Extractor.flipFlopOpposite_false_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) (μ ν : 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) (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 J := 2 ^ (2 ^ 142 * L); have M := ↑(Fintype.card (Fin (matchedBlockSeedBits L) → Bool)); have N := ↑(Fintype.card (Fin (matchedBlockOutputBits 64 L) → Bool)); have ε := (2 ^ e)⁻¹; have ρ := 2 * ε + δ + ↑K * ∑ z : Z, μ z + ↑J * N ^ 2 * ∑ z : Z, ν z; weightDist (flipFlopOppositeWeight n m L e w l r x x' y y' q q' false) (uniformSecondWeight (flipFlopOppositeWeight n m L e w l r x x' y y' q q' false)) ≤ 2 * ρ + 4 * ε + ↑K * (1 + M ^ 2) * M ^ 4 * ∑ z : Z, μ z + ↑K * M ^ 2 / N + ↑J * N ^ 5 * ∑ z : Z, ν z

The complete actual false-versus-true execution is close to its own retained marginal times a uniform final state, from original source envelopes and the original prefix error.