Actual smooth-source middle extraction in an affine round

The old honest left row need only be close to uniform jointly with the selected tampered rows in T. The first right seed is compared with uniform using the actual prefix transcript and tampered seeds in S. The actual middle-left extraction then retains the complete middle-right transcript, original right state, and all tampered outputs in S ∪ T. Overlapping subsets are permitted. Its bound charges the extractor error, the two old discrepancies, and the exact finite prefix/leakage cost.

The checked XOR identity transfers the same bound to the executed masked short rows. Dropping the original right state gives the exact next seed law. These are finite steps in Chattopadhyay--Liao, Extractors for Sum of Two Sources, Theorem 6.1: https://arxiv.org/abs/2110.12652. The complete subset induction and global parameter schedule are separate.

theorem Algebraic.Cutwidth.Extractor.affineRoundMiddleLeftRowsWeight_probability (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) (U : Finset (Fin t)) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affineRoundMiddleLeftRowsWeight d h t L e w l r wl wr ys U)

Original normalized factors give normalized unmasked middle rows.

theorem Algebraic.Cutwidth.Extractor.affineRoundMiddleRowsWeight_probability (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) (U : Finset (Fin t)) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affineRoundMiddleRowsWeight d h t L e w l r wl wr ys U)

The executed masked middle rows define a probability law.

theorem Algebraic.Cutwidth.Extractor.affineRoundMiddleSeedInputWeight_probability (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) (U : Finset (Fin t)) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affineRoundMiddleSeedInputWeight d h t L e w l r wl wr ys U)

The next actual seed-input law is normalized, including null transcript rows.

theorem Algebraic.Cutwidth.Extractor.affineRoundMiddleSeedInputWeight_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) (U : Finset (Fin t)) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : mapWeight (fun (p : ((AffineRoundMiddleRightTranscript Z t L × B) × (↥U → Fin (matchedBlockSeedBits L) → Bool)) × (Fin (matchedBlockSeedBits L) → Bool)) => ((p.1.1.1, p.1.2), p.2)) (affineRoundMiddleRowsWeight d h t L e w l r wl wr ys U) = affineRoundMiddleSeedInputWeight d h t L e w l r wl wr ys U

Dropping the original right state gives exactly the conditional seed-input law.

theorem Algebraic.Cutwidth.Extractor.affineRound_middle_mask_dist_le (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) (U : Finset (Fin t)) : weightDist (affineRoundMiddleRowsWeight d h t L e w l r wl wr ys U) (uniformSecondWeight (affineRoundMiddleRowsWeight d h t L e w l r wl wr ys U)) ≤ weightDist (affineRoundMiddleLeftRowsWeight d h t L e w l r wl wr ys U) (uniformSecondWeight (affineRoundMiddleLeftRowsWeight d h t L e w l r wl wr ys U))

Transcript-dependent masking costs no additional uniformity error.

theorem Algebraic.Cutwidth.Extractor.affineRound_middle_left_dist_le (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 T : Finset (Fin t)) {ρ δ : ℝ} (length : Nat.clog 2 (matchedBlockOutputBits h L + 1) ≤ L) (room : 64 ≤ L) (error : e + 24 + 2 ≤ L) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (source : weightDist (affineRoundLeftRowsWeight h t L w l wl T) (uniformSecondWeight (affineRoundLeftRowsWeight h t L w l wl T)) ≤ ρ) (seed : weightDist (affineRoundMiddleSeedWeight d h t L e w l r wl wr ys S) (uniformSecondWeight (affineRoundMiddleSeedWeight d h t L e w l r wl wr ys S)) ≤ δ) : weightDist (affineRoundMiddleLeftRowsWeight d h t L e w l r wl wr ys (S ∪ T)) (uniformSecondWeight (affineRoundMiddleLeftRowsWeight d h t L e w l r wl wr ys (S ∪ T))) ≤ (2 ^ e)⁻¹ + δ + ρ + 2 ^ (2 ^ 62 * L) * ↑(Fintype.card (Fin (matchedBlockSeedBits L) → Bool)) ^ S.card * ↑(Fintype.card (AffineRoundShortMessages t L)) / ↑(Fintype.card (Fin (matchedBlockOutputBits h L) → Bool))

Actual middle-left extraction merges smooth independence on arbitrary overlapping subsets.

theorem Algebraic.Cutwidth.Extractor.affineRound_middle_dist_le (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 T : Finset (Fin t)) {ρ δ : ℝ} (length : Nat.clog 2 (matchedBlockOutputBits h L + 1) ≤ L) (room : 64 ≤ L) (error : e + 24 + 2 ≤ L) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (source : weightDist (affineRoundLeftRowsWeight h t L w l wl T) (uniformSecondWeight (affineRoundLeftRowsWeight h t L w l wl T)) ≤ ρ) (seed : weightDist (affineRoundMiddleSeedWeight d h t L e w l r wl wr ys S) (uniformSecondWeight (affineRoundMiddleSeedWeight d h t L e w l r wl wr ys S)) ≤ δ) : weightDist (affineRoundMiddleRowsWeight d h t L e w l r wl wr ys (S ∪ T)) (uniformSecondWeight (affineRoundMiddleRowsWeight d h t L e w l r wl wr ys (S ∪ T))) ≤ (2 ^ e)⁻¹ + δ + ρ + 2 ^ (2 ^ 62 * L) * ↑(Fintype.card (Fin (matchedBlockSeedBits L) → Bool)) ^ S.card * ↑(Fintype.card (AffineRoundShortMessages t L)) / ↑(Fintype.card (Fin (matchedBlockOutputBits h L) → Bool))

The actual masked short rows satisfy the same union bound with the full right state retained.

theorem Algebraic.Cutwidth.Extractor.affineRound_middle_seed_input_dist_le (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 T : Finset (Fin t)) {ρ δ : ℝ} (length : Nat.clog 2 (matchedBlockOutputBits h L + 1) ≤ L) (room : 64 ≤ L) (error : e + 24 + 2 ≤ L) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (source : weightDist (affineRoundLeftRowsWeight h t L w l wl T) (uniformSecondWeight (affineRoundLeftRowsWeight h t L w l wl T)) ≤ ρ) (seed : weightDist (affineRoundMiddleSeedWeight d h t L e w l r wl wr ys S) (uniformSecondWeight (affineRoundMiddleSeedWeight d h t L e w l r wl wr ys S)) ≤ δ) : weightDist (affineRoundMiddleSeedInputWeight d h t L e w l r wl wr ys (S ∪ T)) (uniformSecondWeight (affineRoundMiddleSeedInputWeight d h t L e w l r wl wr ys (S ∪ T))) ≤ (2 ^ e)⁻¹ + δ + ρ + 2 ^ (2 ^ 62 * L) * ↑(Fintype.card (Fin (matchedBlockSeedBits L) → Bool)) ^ S.card * ↑(Fintype.card (AffineRoundShortMessages t L)) / ↑(Fintype.card (Fin (matchedBlockOutputBits h L) → Bool))

The actual seed-input law for the second right call satisfies the same union bound.