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

The actual output is nearly uniform given the complete two-pass transcript, its opposite-advice tampered final output, and the entire original left state. Honest and tampered variables on either side may be arbitrarily correlated. The two original side kernels factor given the original transcript. The only security hypotheses concern the original honest source envelopes, the original right look-ahead input envelope, and its initial prefix discrepancy.

The first honest refresh, retaining the tampered refresh, has error ρ. The tampered right coordinate is observed exactly; a correlated repair makes the honest coordinate uniform given that transcript while preserving both original sources. The terminal refresh then uses a left-only tampered seed. Returning to the actual retained marginal costs 2 * ρ. Both refreshes reread the original right source. The left and right observation losses yield the displayed M^5 and N^5 terms, without any independent refreshed-source assumption.

This is the second advice orientation of Chattopadhyay--Goyal--Li's Algorithm 1 and Lemma 6.8, Section 6.3, https://arxiv.org/pdf/1505.00107. The matched-width programs and conservative finite error accounting are this library's checked specialization. Advice.Extraction proves the complete advice-chain guarantee (adviceCorrelationBreaker_dist_le).

theorem Algebraic.Cutwidth.Extractor.flipFlopOpposite_true_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) (state_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) (state_cap : ∀ (z : Z) (q₀ : Fin (matchedBlockOutputBits 64 L) → Bool), w z * mapWeight (q z) (r z) q₀ ≤ ν 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 ρ := 4 * ε + δ + ↑K * (1 + M ^ 2) * ∑ z : Z, μ z + ↑K * M ^ 2 * ∑ z : Z, ν z + ↑J * N ^ 3 * ∑ z : Z, ξ z; weightDist (flipFlopOppositeWeight n m L e w l r x x' y y' q q' true) (uniformSecondWeight (flipFlopOppositeWeight n m L e w l r x x' y y' q q' true)) ≤ 2 * ρ + 2 * ε + ↑K * M ^ 5 * ∑ z : Z, μ z + ↑J * N ^ 5 * ∑ z : Z, ξ z

The complete actual true-versus-false execution is close to its own retained marginal times a uniform final state, with only original source and prefix hypotheses.