Actual advice correlation breaking after a right observation

The original right side supplies the source, while an observed message allows the original left side to supply a jointly near-uniform seed. The complete advice program retains the full original left state and its actual tampered output. The original source envelope pays for the message alphabet; the seed discrepancy is charged only once.

This discharges the conditional source/seed reversal used by the first phase of Chattopadhyay--Liao Theorem 6.1, https://arxiv.org/abs/2110.12652. The seed estimate is a premise of this local composition theorem and must be proved for its preceding extraction.

theorem Algebraic.Cutwidth.Extractor.alternatingAdviceWeight_eq_factored (n m L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} {V : Type u_4} [Fintype Z] [Fintype A] [Fintype B] [Fintype V] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (v : Z → B → V) (s s' : Z × V → A → Fin m → Bool) (x x' : Z → B → Fin n → Bool) (advice advice' : List Bool) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : alternatingAdviceWeight n m L e w l r v s s' x x' advice advice' = adviceCorrelationBreakerWeight n m L e (observedTranscriptWeight w r v) (observedTranscriptKernel r v) (fun (zv : Z × V) => l zv.1) (fun (zv : Z × V) => x zv.1) (fun (zv : Z × V) => x' zv.1) s s' advice advice'

The actual original-law image has the observed and swapped source factors.

theorem Algebraic.Cutwidth.Extractor.alternatingAdviceWeight_probability (n m L e : ℕ) {Z : Type u_1} {A : Type u_2} {B : Type u_3} {V : Type u_4} [Fintype Z] [Fintype A] [Fintype B] [Fintype V] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (v : Z → B → V) (s s' : Z × V → A → Fin m → Bool) (x x' : Z → B → Fin n → Bool) (advice advice' : List Bool) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (alternatingAdviceWeight n m L e w l r v s s' x x' advice advice')

Normalized original factors give a normalized actual advice-breaker output.

theorem Algebraic.Cutwidth.Extractor.alternatingAdvice_dyadic_dist_le (n m L target : ℕ) {Z A B : Type u} {V : Type} [Fintype Z] [Fintype A] [Fintype B] [Fintype V] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (v : Z → B → V) (s s' : Z × V → A → Fin m → Bool) (x x' : Z → B → Fin n → 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) (r z) x₀ ≤ μ z) (seed : weightDist (alternatingSeedWeight w l r v s) (uniformSecondWeight (alternatingSeedWeight w l r v s)) ≤ ρ) (length : advice.length = advice'.length) (different : advice ≠ advice') (source_budget : ↑(Fintype.card V) * ∑ z : Z, μ z ≤ (2 ^ (2 ^ 150 * (advice.length + 1) * L))⁻¹) (seed_width : 2 ^ 150 * (advice.length + 1) * L ≤ m) : have e := adviceErrorExponent advice.length target; have actual := alternatingAdviceWeight n m L e w l r v s s' x x' advice advice'; weightDist actual (uniformSecondWeight actual) ≤ ρ + (2 ^ target)⁻¹

An observed source envelope and actual left-seed error control the full advice call.