Concrete global reserves for repeated affine rounds

The unchanged first-phase chooser, at target target + clog₂(t+1) + 1, pays every round after doubling its original-left entropy reserve. The theorems account for the full initial transcript and two left/four right short-message families per round. All four worst-case subset reserves hold without additional numerical hypotheses.

These are finite parameter deductions for the subset-doubling construction of Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), Theorem 6.1, https://arxiv.org/abs/2110.12652. They do not assert source capacity for every input width or replace the actual statistical iteration proof.

theorem Algebraic.Cutwidth.Extractor.affineIterationRounds_le (t : ℕ) : affineIterationRounds t ≤ t

The number of rounds is no larger than the number of tampered copies.

theorem Algebraic.Cutwidth.Extractor.affineIterationRounds_cover (t : ℕ) : t + 1 ≤ 2 ^ affineIterationRounds t

The doubled subset capacity covers every tampered index, including the zero-copy case.

theorem Algebraic.Cutwidth.Extractor.affineIterationParameters_left_budget (n t a target : ℕ) : have σ := affineIterationTarget t target; have L := affinePhaseOneScale n t a σ; have h := growingMatchedBlockDepth t; affineIterationInitialLeftLoss n t a target + 2 * affineIterationRounds t * affineIterationMessageBits n t a target + 2 ^ (2 * h + 14) * L + t * matchedBlockOutputBits h L + affinePhaseOneLocalError σ ≤ affineIterationSourceEntropy n t a target

A single original-left budget includes the complete initial and repeated observations.

theorem Algebraic.Cutwidth.Extractor.affineIterationParameters_right_budget (n t a target : ℕ) : have σ := affineIterationTarget t target; have L := affinePhaseOneScale n t a σ; affineIterationInitialRightLoss n t a target + 4 * affineIterationRounds t * affineIterationMessageBits n t a target + 2 ^ 62 * L + affinePhaseOneLocalError σ ≤ affinePhaseOneRightBits n t a σ

The existing right-source width pays the complete initial and repeated observations.

theorem Algebraic.Cutwidth.Extractor.affineIterationParameters_left_capacity (n t a target : ℕ) {i : ℕ} (index : i ≤ affineIterationRounds t) : affineIterationInitialLeftLoss n t a target + 2 * i * affineIterationMessageBits n t a target ≤ affineIterationSourceEntropy n t a target

Cumulative left transcript losses never exhaust the original source reserve.

theorem Algebraic.Cutwidth.Extractor.affineIterationParameters_right_capacity (n t a target : ℕ) {i : ℕ} (index : i ≤ affineIterationRounds t) : affineIterationInitialRightLoss n t a target + 4 * i * affineIterationMessageBits n t a target ≤ affinePhaseOneRightBits n t a (affineIterationTarget t target)

Cumulative right transcript losses never exceed the original uniform width.

theorem Algebraic.Cutwidth.Extractor.affineIterationParameters_first_reserve (n t a target : ℕ) {i : ℕ} (index : i < affineIterationRounds t) : have σ := affineIterationTarget t target; have L := affinePhaseOneScale n t a σ; 2 ^ 62 * L + (t + t + 1) * matchedBlockSeedBits L + affinePhaseOneLocalError σ ≤ affineIterationRightEntropy n t a target i

The first short extraction has enough remaining original-right entropy in every round.

theorem Algebraic.Cutwidth.Extractor.affineIterationParameters_merge_reserve (n t a target : ℕ) : have σ := affineIterationTarget t target; have L := affinePhaseOneScale n t a σ; 2 ^ 62 * L + (t + t + 1) * matchedBlockSeedBits L + affinePhaseOneLocalError σ ≤ matchedBlockOutputBits (growingMatchedBlockDepth t) L

The actual long row pays the middle extraction and every selected short output.

theorem Algebraic.Cutwidth.Extractor.affineIterationParameters_recover_reserve (n t a target : ℕ) {i : ℕ} (index : i < affineIterationRounds t) : have σ := affineIterationTarget t target; have L := affinePhaseOneScale n t a σ; 2 ^ 62 * L + (t + 3 * (t + 1)) * matchedBlockSeedBits L + affinePhaseOneLocalError σ ≤ affineIterationRightEntropy n t a target i

The recovery call pays all three right-message families and the selected outputs.

theorem Algebraic.Cutwidth.Extractor.affineIterationParameters_final_reserve (n t a target : ℕ) {i : ℕ} (index : i < affineIterationRounds t) : have σ := affineIterationTarget t target; have L := affinePhaseOneScale n t a σ; have h := growingMatchedBlockDepth t; 2 ^ (2 * h + 14) * L + t * matchedBlockOutputBits h L + 2 * (t + 1) * matchedBlockSeedBits L + affinePhaseOneLocalError σ ≤ affineIterationLeftEntropy n t a target i

The final extraction pays the current selected long outputs and both left observations.

theorem Algebraic.Cutwidth.Extractor.affineIterationParameters_left_mass (n t a target : ℕ) {i : ℕ} (index : i ≤ affineIterationRounds t) : (2 ^ affineIterationMessageBits n t a target) ^ (2 * i) * (2 ^ affineIterationInitialLeftLoss n t a target * (2 ^ affineIterationSourceEntropy n t a target)⁻¹) = (2 ^ affineIterationLeftEntropy n t a target i)⁻¹

Exact dyadic mass after the initial left transcript and two message families per round.

theorem Algebraic.Cutwidth.Extractor.affineIterationParameters_right_mass (n t a target : ℕ) {i : ℕ} (index : i ≤ affineIterationRounds t) : (2 ^ affineIterationMessageBits n t a target) ^ (4 * i) * (2 ^ affineIterationInitialRightLoss n t a target * (2 ^ affinePhaseOneRightBits n t a (affineIterationTarget t target))⁻¹) = (2 ^ affineIterationRightEntropy n t a target i)⁻¹

Exact dyadic mass after the initial right transcript and four message families per round.

theorem Algebraic.Cutwidth.Extractor.affineIterationParameters_error_budget (t target : ℕ) : have R := affineIterationRounds t; have σ := affineIterationTarget t target; 2 ^ R * (2 ^ σ)⁻¹ + 8 * (2 ^ R - 1) * (2 ^ affinePhaseOneLocalError σ)⁻¹ ≤ (2 ^ target)⁻¹

The complete ρ ↦ 2ρ + 8 * 2⁻ᵉ recurrence fits the requested final error.

theorem Algebraic.Cutwidth.Extractor.affineIterationParameters_phase_one_reserve (n t a target : ℕ) : affinePhaseOneSourceEntropy n t a (affineIterationTarget t target) ≤ affineIterationSourceEntropy n t a target

The doubled source reserve also satisfies the original first-phase entropy hypothesis.

theorem Algebraic.Cutwidth.Extractor.affineIterationParameters_entropy_le (n t a target : ℕ) : affineIterationSourceEntropy n t a target ≤ 2 ^ 257 * (t + 1) ^ 2 * (a + 1) * affinePhaseOneBase n t a (affineIterationTarget t target) ^ 2

The full original-left entropy reserve remains a fixed polynomial in the chooser base.