Final extraction against a finite set of actual round outputs

The actual honest final seed is close to uniform given the middle transcript and selected tampered seeds. The original left-source joint envelope then bounds the actual final growing matched extraction, retaining the complete round transcript, the entire original right state, and all selected next rows. The envelope cost is the square of the short-message alphabet size; the selected outputs cost their tuple's alphabet size. No cap on individual conditional rows or per-transcript seed-error bound is required.

The actual masked rows have the same bound. Projecting away the original right state gives the exact left-row law used as the next round's input. This is the fourth-call consumer in Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), Theorem 6.1, printed pp.23--25, using Lemma 3.26, printed p.15: https://arxiv.org/abs/2110.12652. Producing its actual seed discrepancy is a separate extraction step; no complete correlation breaker is asserted by this local theorem.

theorem Algebraic.Cutwidth.Extractor.affineRoundFinalSeedWeight_eq_map (d h t L e : ℕ) {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 → ℝ) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (S : Finset (Fin t)) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : affineRoundFinalSeedWeight d h t L e w l r wl wr ys S = mapWeight (fun (p : (Z × B) × A) => have seeds := fun (i : Option (Fin t)) => affineRoundFinalSeed d h L e (ys p.1.1 p.1.2 i) fun (j : Fin (matchedBlockOutputBits h L)) => wl p.1.1 p.2 i j ^^ wr p.1.1 p.1.2 i j; ((affineRoundMiddleTranscript d h t L e wl wr ys p, fun (i : ↥S) => seeds (some ↑i)), seeds none)) (factoredWeight w l r)

The conditional final-seed law is exactly an image of the original source law.

theorem Algebraic.Cutwidth.Extractor.affineRoundLeftSubsetWeight_probability (n d h t L e : ℕ) {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) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (S : Finset (Fin t)) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affineRoundLeftSubsetWeight n d h t L e w l r x wl wr ys S)

Normalized original factors give normalized actual retained left contributions.

theorem Algebraic.Cutwidth.Extractor.affineRoundSubsetWeight_probability (n d h t L e : ℕ) {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) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (S : Finset (Fin t)) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affineRoundSubsetWeight n d h t L e w l r x mask wl wr ys S)

Normalized original factors give normalized actual retained masked next rows.

theorem Algebraic.Cutwidth.Extractor.affineRoundSubset_dist_le_left (n d h t L e : ℕ) {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) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (S : Finset (Fin t)) : weightDist (affineRoundSubsetWeight n d h t L e w l r x mask wl wr ys S) (uniformSecondWeight (affineRoundSubsetWeight n d h t L e w l r x mask wl wr ys S)) ≤ weightDist (affineRoundLeftSubsetWeight n d h t L e w l r x wl wr ys S) (uniformSecondWeight (affineRoundLeftSubsetWeight n d h t L e w l r x wl wr ys S))

Applying the actual right masks costs no additional conditional-uniformity error.

theorem Algebraic.Cutwidth.Extractor.affineRoundNextLeftRows_eq_map (n d h t L e : ℕ) {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) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (S : Finset (Fin t)) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : affineRoundLeftRowsWeight h t L (affineRoundTranscriptWeight d h t L e w l r wl wr ys) (affineRoundTranscriptLeft h t L e l wl) (affineRoundOutputLeft n h t L e x) S = mapWeight (fun (p : ((AffineRoundTranscript Z t L × B) × (↥S → Fin (matchedBlockOutputBits h L) → Bool)) × (Fin (matchedBlockOutputBits h L) → Bool)) => ((p.1.1.1, p.1.2), p.2)) (affineRoundLeftSubsetWeight n d h t L e w l r x wl wr ys S)

Discarding original B gives exactly the next round's left-row subset law.

theorem Algebraic.Cutwidth.Extractor.affineRoundNextLeftRows_dist_le (n d h t L e : ℕ) {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) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (S : Finset (Fin t)) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : weightDist (affineRoundLeftRowsWeight h t L (affineRoundTranscriptWeight d h t L e w l r wl wr ys) (affineRoundTranscriptLeft h t L e l wl) (affineRoundOutputLeft n h t L e x) S) (uniformSecondWeight (affineRoundLeftRowsWeight h t L (affineRoundTranscriptWeight d h t L e w l r wl wr ys) (affineRoundTranscriptLeft h t L e l wl) (affineRoundOutputLeft n h t L e x) S)) ≤ weightDist (affineRoundLeftSubsetWeight n d h t L e w l r x wl wr ys S) (uniformSecondWeight (affineRoundLeftSubsetWeight n d h t L e w l r x wl wr ys S))

The next left-row subset discrepancy is no larger than the retained final-call discrepancy.

theorem Algebraic.Cutwidth.Extractor.affineRoundLeftSubset_dist_le (n d h t 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) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (S : Finset (Fin t)) (μ : 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 (affineRoundFinalSeedWeight d h t L e w l r wl wr ys S) (uniformSecondWeight (affineRoundFinalSeedWeight d h t L e w l r wl wr ys S)) ≤ δ) : weightDist (affineRoundLeftSubsetWeight n d h t L e w l r x wl wr ys S) (uniformSecondWeight (affineRoundLeftSubsetWeight n d h t L e w l r x wl wr ys S)) ≤ (2 ^ e)⁻¹ + δ + 2 ^ (2 ^ (2 * h + 14) * L) * ↑(Fintype.card (Fin (matchedBlockOutputBits h L) → Bool)) ^ S.card * ↑(Fintype.card (AffineRoundShortMessages t L)) ^ 2 * ∑ z : Z, μ z

The actual growing extractor preserves uniformity against the selected next left rows.

theorem Algebraic.Cutwidth.Extractor.affineRoundSubset_dist_le (n d h t 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) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (ys : Z → B → AffinePhaseOneCopies t d) (S : Finset (Fin t)) (μ : 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 (affineRoundFinalSeedWeight d h t L e w l r wl wr ys S) (uniformSecondWeight (affineRoundFinalSeedWeight d h t L e w l r wl wr ys S)) ≤ δ) : weightDist (affineRoundSubsetWeight n d h t L e w l r x mask wl wr ys S) (uniformSecondWeight (affineRoundSubsetWeight n d h t L e w l r x mask wl wr ys S)) ≤ (2 ^ e)⁻¹ + δ + 2 ^ (2 ^ (2 * h + 14) * L) * ↑(Fintype.card (Fin (matchedBlockOutputBits h L) → Bool)) ^ S.card * ↑(Fintype.card (AffineRoundShortMessages t L)) ^ 2 * ∑ z : Z, μ z

The same original-source and actual-seed bounds control the masked next rows.