Advice correlation breaking with an approximately uniform right input

The complete actual program retains the full original right state and actual tampered output. Its error increases by only the original joint right-input discrepancy from uniform. The source and tampered program keep their full joint law during a constructed coordinate repair; no repair certificate or worst-case conditional uniformity assumption is supplied.

This is the standard-correlation-breaker input step of Chattopadhyay--Liao, Theorem 6.1, https://arxiv.org/abs/2110.12652. In its affine application the right input here is an earlier extracted value and the left source is the original uniform seed after transcript observations. The theorem itself uses the concrete advice program and its checked finite bounds.

theorem Algebraic.Cutwidth.Extractor.adviceCorrelationBreaker_perturbed_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) (seed : weightDist (retainedSeedWeight w r y) (uniformSecondWeight (retainedSeedWeight w r y)) ≤ ρ) (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 advice program pays the original right-input discrepancy once.

theorem Algebraic.Cutwidth.Extractor.adviceCorrelationBreaker_perturbed_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) (seed : weightDist (retainedSeedWeight w r y) (uniformSecondWeight (retainedSeedWeight w r y)) ≤ ρ) (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)⁻¹

The dyadic guarantee tolerates joint seed error while retaining the actual marginal.