Actual masked prefixes and first right seeds of an affine round

A balanced prefix of the old honest row remains nearly uniform while retaining the selected tampered rows. Observing independent right masks and applying their known XOR values preserves this bound. The following actual right extraction pays its selected output alphabet and the one right prefix-mask observation against the original right-source envelope.

This supplies the first alternating step of Chattopadhyay--Liao, Extractors for Sum of Two Sources, Theorem 6.1: https://arxiv.org/abs/2110.12652.

theorem Algebraic.Cutwidth.Extractor.affineRoundLeftRowsWeight_probability (h t L : ℕ) {Z : Type u_1} {A : Type u_2} [Fintype Z] [Fintype A] (w : Z → ℝ) (l : Z → A → ℝ) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (S : Finset (Fin t)) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) : IsProbabilityWeight (affineRoundLeftRowsWeight h t L w l wl S)

The old retained-subset law is normalized.

theorem Algebraic.Cutwidth.Extractor.affineRoundPrefixSeedWeight_probability (h t 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 → ℝ) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (S : Finset (Fin t)) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affineRoundPrefixSeedWeight h t L w l r wl wr S)

The actual masked-prefix seed law is normalized.

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

The first executed right-seed law is normalized.

theorem Algebraic.Cutwidth.Extractor.affineRoundPrefix_uniform (h L : ℕ) (size : matchedBlockSeedBits L ≤ matchedBlockOutputBits h L) : mapWeight (affineRoundPrefix h L) (uniformWeight (Fin (matchedBlockOutputBits h L) → Bool)) = uniformWeight (Fin (matchedBlockSeedBits L) → Bool)

A long enough prefix maps the uniform row exactly to uniform.

theorem Algebraic.Cutwidth.Extractor.affineRoundPrefixSeed_dist_le (h t L : ℕ) (size : matchedBlockSeedBits L ≤ matchedBlockOutputBits h 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 → ℝ) (wl : Z → A → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (wr : Z → B → AffinePhaseOneCopies t (matchedBlockOutputBits h L)) (S : Finset (Fin t)) (hw : ∀ (z : Z), 0 ≤ w z) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : weightDist (affineRoundPrefixSeedWeight h t L w l r wl wr S) (uniformSecondWeight (affineRoundPrefixSeedWeight h t L w l r wl wr S)) ≤ weightDist (affineRoundLeftRowsWeight h t L w l wl S) (uniformSecondWeight (affineRoundLeftRowsWeight h t L w l wl S))

Actual masked prefixes inherit the old retained-subset discrepancy.

theorem Algebraic.Cutwidth.Extractor.affineRoundMiddleSeed_dist_le (d h t L e : ℕ) (size : matchedBlockSeedBits L ≤ matchedBlockOutputBits h L) (length : Nat.clog 2 (d + 1) ≤ L) (room : 64 ≤ L) (error : e + 24 + 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 → ℝ) (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) (y₀ : Fin d → Bool), w z * mapWeight (fun (b : B) => ys z b none) (r z) y₀ ≤ ν z) (old : weightDist (affineRoundLeftRowsWeight h t L w l wl S) (uniformSecondWeight (affineRoundLeftRowsWeight h t L w l wl S)) ≤ ρ) : 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)) ≤ (2 ^ e)⁻¹ + ρ + 2 ^ (2 ^ 62 * L) * ↑(Fintype.card (Fin (matchedBlockSeedBits L) → Bool)) ^ S.card * ↑(Fintype.card (AffineRoundShortMessages t L)) * ∑ z : Z, ν z

The first actual right extraction follows from the old row and original source envelope.