Security of repeated actual affine rounds

The actual evolving states double their retained-subset capacity, with closed discrepancy 2^i * ρ + 8 * (2^i - 1) * 2^-e. Every intermediate source bound follows from an original envelope and its exact message accounting. No intermediate seed or repaired-source witness is supplied.

The state invariant also bounds the actual XOR outputs while retaining the complete original right state. Appending that conditionally independent state preserves the left-row error; known output masks add no error.

The selected theorem initializes from the actual first phase and supplies all round budgets. Its conclusion concerns the complete named program on the original affine input, retaining the original tag, full right latent state, and any set of tampered outputs, including all tamperings. No intermediate source or seed certificate occurs in its hypotheses. The source reserve is conservative and is not asserted feasible for every input size. This follows the finite construction in Chattopadhyay--Liao, Extractors for Sum of Two Sources, Theorem 6.1: https://arxiv.org/abs/2110.12652.

theorem Algebraic.Cutwidth.Extractor.affineIterationError_zero (e : ℕ) (ρ : ℝ) : affineIterationError e ρ 0 = ρ

Before any round, the discrepancy is the initial discrepancy.

theorem Algebraic.Cutwidth.Extractor.affineIterationError_succ (e i : ℕ) (ρ : ℝ) : affineIterationError e ρ (i + 1) = 2 * affineIterationError e ρ i + 8 * (2 ^ e)⁻¹

One additional round doubles the previous error and adds its local loss.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.iterate_invariant {n d h t L : ℕ} {Z : Type u_4} {A : Type u_5} {B : Type u_6} [Fintype Z] [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (e rounds k : ℕ) (kx ky : ℕ → ℕ) (μ ν : Z → ℝ) {ρ : ℝ} (size : matchedBlockSeedBits L ≤ matchedBlockOutputBits h L) (right_length : Nat.clog 2 (d + 1) ≤ L) (row_length : Nat.clog 2 (matchedBlockOutputBits h L + 1) ≤ L) (room : 64 ≤ L) (short_error : e + 24 + 2 ≤ L) (final_length : Nat.clog 2 (n + 1) ≤ L) (final_error : e + h + 2 ≤ L) (final_budget : (h + 1) * (e + 2 * h + Nat.clog 2 (L + 1) + 4) ≤ L) (hw : IsProbabilityWeight s.weight) (hl : ∀ (z : Z), IsProbabilityWeight (s.left z)) (hr : ∀ (z : Z), IsProbabilityWeight (s.right z)) (left_nonnegative : ∀ (z : Z), 0 ≤ μ z) (right_nonnegative : ∀ (z : Z), 0 ≤ ν z) (left_cap : ∀ (z : Z) (x₀ : Fin n → Bool), s.weight z * mapWeight (s.source z) (s.left z) x₀ ≤ μ z) (right_cap : ∀ (z : Z) (y₀ : Fin d → Bool), s.weight z * mapWeight (fun (b : B) => s.rightWords z b none) (s.right z) y₀ ≤ ν z) (first : ∀ i < rounds, 2 ^ 62 * L + (t + t + 1) * matchedBlockSeedBits L + e ≤ ky i) (merge : 2 ^ 62 * L + (t + t + 1) * matchedBlockSeedBits L + e ≤ matchedBlockOutputBits h L) (recover : ∀ i < rounds, 2 ^ 62 * L + (t + 3 * (t + 1)) * matchedBlockSeedBits L + e ≤ ky i) (final : ∀ i < rounds, 2 ^ (2 * h + 14) * L + t * matchedBlockOutputBits h L + 2 * (t + 1) * matchedBlockSeedBits L + e ≤ kx i) (left_mass : ∀ i < rounds, ↑(Fintype.card (AffineRoundShortMessages t L)) ^ (2 * i) * ∑ z : Z, μ z ≤ (2 ^ kx i)⁻¹) (right_mass : ∀ i < rounds, ↑(Fintype.card (AffineRoundShortMessages t L)) ^ (4 * i) * ∑ z : Z, ν z ≤ (2 ^ ky i)⁻¹) (old : AffineRowInvariant h t L s.weight s.left s.leftRows k ρ) (i : ℕ) (executed : i ≤ rounds) : AffineRowInvariant h t L (s.iterate e i).weight (s.iterate e i).left (s.iterate e i).leftRows (2 ^ i * k) (affineIterationError e ρ i)

Original envelopes and finite reserves propagate the invariant along every actual iterate.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.leftSubsetWeight_dist_eq {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (S : Finset (Fin t)) (hw : ∀ (z : Z), 0 ≤ s.weight z) (hr : ∀ (z : Z), IsProbabilityWeight (s.right z)) : weightDist (s.leftSubsetWeight S) (uniformSecondWeight (s.leftSubsetWeight S)) = weightDist (affineRoundLeftRowsWeight h t L s.weight s.left s.leftRows S) (uniformSecondWeight (affineRoundLeftRowsWeight h t L s.weight s.left s.leftRows S))

Appending the complete conditionally independent right state preserves the left-row error.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.subsetWeight_dist_le_left {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (S : Finset (Fin t)) : weightDist (s.subsetWeight S) (uniformSecondWeight (s.subsetWeight S)) ≤ weightDist (s.leftSubsetWeight S) (uniformSecondWeight (s.leftSubsetWeight S))

The known honest and tampered right masks do not increase the conditional-uniformity error.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.subsetWeight_probability {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (S : Finset (Fin t)) (hw : IsProbabilityWeight s.weight) (hl : ∀ (z : Z), IsProbabilityWeight (s.left z)) (hr : ∀ (z : Z), IsProbabilityWeight (s.right z)) : IsProbabilityWeight (s.subsetWeight S)

Normalized factors induce a normalized actual masked-output law.

theorem Algebraic.Cutwidth.Extractor.AffineIterationState.subsetWeight_dist_le {n d h t L : ℕ} {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (s : AffineIterationState n d h t L Z A B) (S : Finset (Fin t)) {k : ℕ} {ρ : ℝ} (hw : ∀ (z : Z), 0 ≤ s.weight z) (hr : ∀ (z : Z), IsProbabilityWeight (s.right z)) (invariant : AffineRowInvariant h t L s.weight s.left s.leftRows k ρ) (size : S.card ≤ k) : weightDist (s.subsetWeight S) (uniformSecondWeight (s.subsetWeight S)) ≤ ρ

An actual left-row invariant bounds masked outputs while retaining the complete right state.

theorem Algebraic.Cutwidth.Extractor.affineCorrelationBreakerWeight_probability (n d t h L₀ e₀ L₁ e₁ er rounds : ℕ) {Z : Type u_4} {A : Type u_5} {B : Type u_6} [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) (S : Finset (Fin t)) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (affineCorrelationBreakerWeight n d t h L₀ e₀ L₁ e₁ er rounds w l r x mask ys advice S)

The complete actual program induces a normalized original-input output law.

theorem Algebraic.Cutwidth.Extractor.affineCorrelationBreaker_parameters_dist_le (n t a target : ℕ) {Z A B : Type u} [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 (affinePhaseOneRightBits n t a (affineIterationTarget t target))) (advice : Option (Fin t) → List Bool) (S : Finset (Fin t)) (μ : Z → ℝ) (positive : 0 < t) (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) (uniform : ∀ (z : Z), mapWeight (fun (b : B) => ys z b none) (r z) = uniformWeight (Fin (affinePhaseOneRightBits n t a (affineIterationTarget t target)) → Bool)) (honest_length : (advice none).length = a) (tampered_length : ∀ (i : Fin t), (advice (some i)).length = a) (different : ∀ (i : Fin t), advice none ≠ advice (some i)) (source : ∑ z : Z, μ z ≤ (2 ^ affineIterationSourceEntropy n t a target)⁻¹) : let σ := affineIterationTarget t target; let d := affinePhaseOneRightBits n t a σ; have h := growingMatchedBlockDepth t; have L₀ := affinePhaseOneInitialScale n t a σ; have L := affinePhaseOneScale n t a σ; have e := affinePhaseOneLocalError σ; have actual := affineCorrelationBreakerWeight n d t h L₀ e L (adviceErrorExponent a e) e (affineIterationRounds t) w l r x mask ys advice S; weightDist actual (uniformSecondWeight actual) ≤ (2 ^ target)⁻¹

The chosen complete affine program has the requested error against every tampering subset.