Actual final pairwise extraction in the first affine phase

The preceding actual second-seed discrepancy supplies the only intermediate statistical premise. From the original normalized source factors and its joint left-source envelope, the actual growing matched extractor gives pairwise output security while retaining the complete transcript and original right state. The envelope pays for all first extraction outputs and one tampered final output. No individual transcript row is required to have a uniform seed or a capped conditional source.

The left-contribution law supports later merging rounds. The actual masked pair has the same bound because both masks are determined by the retained transcript and original right state. This is a local consumer of the preceding seed bound, not the full affine correlation-breaker theorem or a simultaneous guarantee against every tampered output.

The construction and pairwise merging step follow Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), Theorem 6.1, printed p.23, and Lemma 3.26, printed p.15: https://arxiv.org/abs/2110.12652.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOnePair_dist_le_left (n d t h L₀ e₀ L₁ e₁ er : ℕ) {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) (ys : Z → B → AffinePhaseOneCopies t d) (advice : Option (Fin t) → List Bool) (i : Fin t) : weightDist (affinePhaseOnePairWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice i) (uniformSecondWeight (affinePhaseOnePairWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice i)) ≤ weightDist (affinePhaseOneLeftPairWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice i) (uniformSecondWeight (affinePhaseOneLeftPairWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice i))

Masking both final values does not increase the distance from retained-tag uniformity.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneLeftPairWeight_probability (n d t h L₀ e₀ L₁ e₁ er : ℕ) {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) (ys : Z → B → AffinePhaseOneCopies t d) (advice : Option (Fin t) → List Bool) (i : Fin t) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affinePhaseOneLeftPairWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice i)

The original normalized factors give a normalized retained left-contribution pair.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOnePairWeight_probability (n d t h L₀ e₀ L₁ e₁ er : ℕ) {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) (ys : Z → B → AffinePhaseOneCopies t d) (advice : Option (Fin t) → List Bool) (i : Fin t) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affinePhaseOnePairWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice i)

The original normalized factors give a normalized retained actual masked pair.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOneLeftPair_dist_le (n d t h L₀ e₀ L₁ e₁ er : ℕ) (length : Nat.clog 2 (n + 1) ≤ L₁) (error : er + h + 2 ≤ L₁) (budget : (h + 1) * (er + 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) (ys : Z → B → AffinePhaseOneCopies t d) (advice : Option (Fin t) → List Bool) (i : 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 (affinePhaseOneSecondSeedWeight n d t L₀ e₀ L₁ e₁ w l r x mask ys advice i) (uniformSecondWeight (affinePhaseOneSecondSeedWeight n d t L₀ e₀ L₁ e₁ w l r x mask ys advice i)) ≤ δ) : weightDist (affinePhaseOneLeftPairWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice i) (uniformSecondWeight (affinePhaseOneLeftPairWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice i)) ≤ (2 ^ er)⁻¹ + δ + 2 ^ (2 ^ (2 * h + 14) * L₁) * ↑(Fintype.card (Fin (matchedBlockOutputBits h L₁) → Bool)) * ↑(Fintype.card (AffinePhaseOneCopies t (matchedBlockOutputBits 64 L₀))) * ∑ z : Z, μ z

The actual growing extractor merges the preceding second-seed pair into left contributions.

theorem Algebraic.Cutwidth.Extractor.affinePhaseOnePair_dist_le (n d t h L₀ e₀ L₁ e₁ er : ℕ) (length : Nat.clog 2 (n + 1) ≤ L₁) (error : er + h + 2 ≤ L₁) (budget : (h + 1) * (er + 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) (ys : Z → B → AffinePhaseOneCopies t d) (advice : Option (Fin t) → List Bool) (i : 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 (affinePhaseOneSecondSeedWeight n d t L₀ e₀ L₁ e₁ w l r x mask ys advice i) (uniformSecondWeight (affinePhaseOneSecondSeedWeight n d t L₀ e₀ L₁ e₁ w l r x mask ys advice i)) ≤ δ) : weightDist (affinePhaseOnePairWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice i) (uniformSecondWeight (affinePhaseOnePairWeight n d t h L₀ e₀ L₁ e₁ er w l r x mask ys advice i)) ≤ (2 ^ er)⁻¹ + δ + 2 ^ (2 ^ (2 * h + 14) * L₁) * ↑(Fintype.card (Fin (matchedBlockOutputBits h L₁) → Bool)) * ↑(Fintype.card (AffinePhaseOneCopies t (matchedBlockOutputBits 64 L₀))) * ∑ z : Z, μ z

The actual masked final pair satisfies the same bound, without an additional masking error.