Actual matched extraction with a correlated right mask

The honest source is XORed with a mask carried by the original right state. Matched extraction retains that full state, with the same finite entropy budget as the unmasked source and one charge for seed discrepancy. The actual program's fixed-seed XOR identity discharges the linearity premise.

The depth-sixty-four call seeds the standard correlation breaker in the first phase of Chattopadhyay--Liao Theorem 6.1; growing depths provide longer rows for its later independence-merging phase: https://arxiv.org/abs/2110.12652.

theorem Algebraic.Cutwidth.Extractor.matchedBlockExtractor_depth64_affine_dist_le (n L e : ℕ) (length : Nat.clog 2 (n + 1) ≤ L) (room : 64 ≤ L) (error : e + 64 + 2 ≤ L) {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 : Z → A → Fin n → Bool) (mask : Z → B → Fin n → Bool) (y : Z → B → Fin (matchedBlockSeedBits L) → 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)) ≤ δ) : have actual := affineExtractionWeight w l r x mask y (fun (a b : Fin n → Bool) (i : Fin n) => a i ^^ b i) (matchedBlockExtractor n 64 L e); weightDist actual (uniformSecondWeight actual) ≤ (2 ^ e)⁻¹ + δ + 2 ^ (2 ^ 142 * L) * ∑ z : Z, μ z

The actual long initial extraction retains the correlated right mask and complete state.

theorem Algebraic.Cutwidth.Extractor.matchedBlockExtractor_growing_affine_dist_le (n h L e : ℕ) (length : Nat.clog 2 (n + 1) ≤ L) (error : e + h + 2 ≤ L) (budget : (h + 1) * (e + 2 * h + Nat.clog 2 (L + 1) + 4) ≤ L) {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 : Z → A → Fin n → Bool) (mask : Z → B → Fin n → Bool) (y : Z → B → Fin (matchedBlockSeedBits L) → 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)) ≤ δ) : have actual := affineExtractionWeight w l r x mask y (fun (a b : Fin n → Bool) (i : Fin n) => a i ^^ b i) (matchedBlockExtractor n h L e); weightDist actual (uniformSecondWeight actual) ≤ (2 ^ e)⁻¹ + δ + 2 ^ (2 ^ (2 * h + 14) * L) * ∑ z : Z, μ z

Growing output rows retain the same strong guarantee under a correlated source mask.