Strong extraction by the complete concrete advice chain

Unequal advice of equal length makes the actual honest output close to uniform, jointly with the actual tampered output and the entire original right state. Inputs are independent conditional on the shared tag. The honest right input is uniform on each row; the left input has the stated average point-mass envelope. Tampered inputs are arbitrary functions of those same original left and right states.

The proof constructs every intermediate invariant from the input law. The finite dyadic corollary pays the conservative per-bit error amplification with an explicit entropy reserve and local error schedule. Chattopadhyay, Goyal, and Li supply the advice-chain strategy in Algorithm 2, Section 6.3 of https://arxiv.org/abs/1505.00107; the additional final extraction from the original left source retains the full original right state.

theorem Algebraic.Cutwidth.Extractor.adviceCorrelationBreaker_dist_le (n m L e : ℕ) {Z A B : Type u} [Fintype Z] [Fintype A] [Fintype B] (guard : FlipFlopSizeGuard n m L e) (size : matchedBlockOutputBits 64 L ≤ m) (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → Fin n → Bool) (y y' : Z → B → Fin m → Bool) (advice advice' : List 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) (uniform : ∀ (z : Z), mapWeight (y z) (r z) = uniformWeight (Fin m → Bool)) (length : advice.length = advice'.length) (different : advice ≠ advice') : have actual := adviceCorrelationBreakerWeight n m L e w l r x x' y y' advice advice'; weightDist actual (uniformSecondWeight actual) ≤ adviceCorrelationBreakerError m L e advice.length (∑ z : Z, μ z)

The actual complete advice program obeys its finite error budget.

theorem Algebraic.Cutwidth.Extractor.adviceCorrelationBreaker_dyadic_dist_le (n m L target : ℕ) {Z A B : Type u} [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) (advice advice' : List Bool) (μ : Z → ℝ) (guard : FlipFlopSizeGuard n m L (adviceErrorExponent advice.length target)) (size : matchedBlockOutputBits 64 L ≤ m) (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) (uniform : ∀ (z : Z), mapWeight (y z) (r z) = uniformWeight (Fin m → Bool)) (length : advice.length = advice'.length) (different : advice ≠ advice') (left : ∑ z : Z, μ z ≤ (2 ^ (2 ^ 150 * (advice.length + 1) * L))⁻¹) (right : 2 ^ 150 * (advice.length + 1) * L ≤ m) : have e := adviceErrorExponent advice.length target; have actual := adviceCorrelationBreakerWeight n m L e w l r x x' y y' advice advice'; weightDist actual (uniformSecondWeight actual) ≤ (2 ^ target)⁻¹

An explicit entropy reserve and error schedule give the requested dyadic error.