Finite splitting and resource bounds for the near-halving schedule

The depth-dependent rate and entropy reserve certify both splitting inequalities at every executed level. One initial logarithmic budget bounds all actual rounded widths and field seeds. The full seed estimate includes the final one-shot pair shared by all leaves. Total block payload stays at most twice the initial width, and positive reserve bounds block counts too.

The entropy requirements are those of Chattopadhyay--Goodman--Liao, Corollary 5.4 of Affine Extractors for Almost Logarithmic Entropy, https://eccc.weizmann.ac.il/report/2021/075/. This schedule and its finite arithmetic estimates are deductions from the checked paired-condenser API. No asymptotic parameter choice or full runtime bound is asserted here.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockEntropy_succ (h Q : ℕ) {i : ℕ} (level : i < h) : nearHalvingBlockEntropy h Q i = 2 * nearHalvingBlockEntropy h Q (i + 1) + 2 ^ (h - i) * Q

Each split retains half the entropy after paying its exact reserve gap.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockEntropy_le_initial (h Q i : ℕ) : nearHalvingBlockEntropy h Q i ≤ nearHalvingBlockEntropy h Q 0

Every scheduled entropy threshold is bounded by the initial threshold.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockEntropy_last (h Q : ℕ) : nearHalvingBlockEntropy h Q h = (8 * h + 8) * Q

The final entropy threshold is the depth-adjusted leaf reserve.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockWidth_bounds (N h Q E : ℕ) (capacity : nearHalvingBlockEntropy h Q 0 ≤ N) (reserve : 2 * (6 * (nearHalvingBlockRate h + 1) * explicitCondenserBudget N (nearHalvingBlockEntropy h Q 0) E + 2 * E) ≤ Q) {i : ℕ} (level : i ≤ h) : nearHalvingBlockEntropy h Q i ≤ nearHalvingBlockWidth N h Q E i ∧ nearHalvingBlockWidth N h Q E i ≤ N

Every executed block holds its entropy and fits within the initial width.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlock_split_budget (N h Q E : ℕ) (capacity : nearHalvingBlockEntropy h Q 0 ≤ N) (reserve : 2 * (6 * (nearHalvingBlockRate h + 1) * explicitCondenserBudget N (nearHalvingBlockEntropy h Q 0) E + 2 * E) ≤ Q) {i : ℕ} (level : i < h) : nearHalvingBlockEntropy h Q (i + 1) ≤ nearHalvingBlockWidth N h Q E (i + 1) ∧ nearHalvingBlockWidth N h Q E (i + 1) + nearHalvingBlockEntropy h Q (i + 1) + E ≤ nearHalvingBlockEntropy h Q i

The global reserve certifies both entropy inequalities at every split.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlock_split_budget_of_bound (N h Q E T : ℕ) (capacity : nearHalvingBlockEntropy h Q 0 ≤ N) (common : explicitCondenserBudget N (nearHalvingBlockEntropy h Q 0) E ≤ T) (reserve : 12 * (nearHalvingBlockRate h + 1) * T + 4 * E ≤ Q) {i : ℕ} (level : i < h) : nearHalvingBlockEntropy h Q (i + 1) ≤ nearHalvingBlockWidth N h Q E (i + 1) ∧ nearHalvingBlockWidth N h Q E (i + 1) + nearHalvingBlockEntropy h Q (i + 1) + E ≤ nearHalvingBlockEntropy h Q i

A supplied upper bound on the initial budget certifies all split inequalities.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockLeafLength_budget (h Q E : ℕ) (reserve : 2 * E ≤ Q) : nearHalvingBlockLeafLength h Q + 2 * E ≤ nearHalvingBlockEntropy h Q h

One reserve unit pays the final one-shot extractor entropy loss.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockEntropy_mass (h Q : ℕ) {i : ℕ} (level : i ≤ h) : 2 ^ i * nearHalvingBlockEntropy h Q i = 2 ^ h * (8 * h + 8 + (h - i)) * Q

The aggregate entropy has an exact expression at every executed level.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockEntropy_mass_le (h Q : ℕ) {i : ℕ} (level : i ≤ h) : 2 ^ i * nearHalvingBlockEntropy h Q i ≤ nearHalvingBlockEntropy h Q 0

The sum of the scheduled entropy thresholds never exceeds the initial entropy.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockSeedWidth_le (N h Q E : ℕ) (capacity : nearHalvingBlockEntropy h Q 0 ≤ N) (reserve : 2 * (6 * (nearHalvingBlockRate h + 1) * explicitCondenserBudget N (nearHalvingBlockEntropy h Q 0) E + 2 * E) ≤ Q) {i : ℕ} (level : i ≤ h) : nearHalvingBlockSeedWidth N h Q E i ≤ 6 * (nearHalvingBlockRate h + 1) * explicitCondenserBudget N (nearHalvingBlockEntropy h Q 0) E

The initial logarithmic budget bounds every actual internal field seed.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlock_payload_le (N h Q E : ℕ) (capacity : nearHalvingBlockEntropy h Q 0 ≤ N) (reserve : 2 * (6 * (nearHalvingBlockRate h + 1) * explicitCondenserBudget N (nearHalvingBlockEntropy h Q 0) E + 2 * E) ≤ Q) {i : ℕ} (level : i ≤ h) : 2 ^ i * nearHalvingBlockWidth N h Q E i ≤ 2 * N

All blocks together occupy at most twice the initial width.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlock_count_le (h Q : ℕ) (positive : 0 < Q) {i : ℕ} (level : i ≤ h) : 2 ^ i ≤ nearHalvingBlockEntropy h Q 0

Positive reserve bounds the number of blocks independently of their widths.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockSeedBits_le (N h Q E : ℕ) (capacity : nearHalvingBlockEntropy h Q 0 ≤ N) (reserve : 2 * (6 * (nearHalvingBlockRate h + 1) * explicitCondenserBudget N (nearHalvingBlockEntropy h Q 0) E + 2 * E) ≤ Q) : nearHalvingBlockSeedBits N h Q E ≤ h * (6 * (nearHalvingBlockRate h + 1) * explicitCondenserBudget N (nearHalvingBlockEntropy h Q 0) E) + (84 * (explicitCondenserBudget N (nearHalvingBlockEntropy h Q 0) E + 1) + 18 * nearHalvingBlockLeafLength h Q + 24 * E + 6)

The complete seed bound includes every internal seed and the shared final pair.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockSeedBits_le_of_bound (N h Q E T : ℕ) (capacity : nearHalvingBlockEntropy h Q 0 ≤ N) (common : explicitCondenserBudget N (nearHalvingBlockEntropy h Q 0) E ≤ T) (reserve : 12 * (nearHalvingBlockRate h + 1) * T + 4 * E ≤ Q) : nearHalvingBlockSeedBits N h Q E ≤ h * (6 * (nearHalvingBlockRate h + 1) * T) + (84 * (T + 1) + 18 * nearHalvingBlockLeafLength h Q + 24 * E + 6)

A common logarithmic budget gives a direct bound on the complete seed.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockOutputBits_accounting (h Q : ℕ) : 9 * nearHalvingBlockOutputBits h Q + 2 ^ h * Q = 8 * nearHalvingBlockEntropy h Q 0

Exact accounting relates total output bits to the initial entropy.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockOutputBits_lower (h Q : ℕ) : 7 * nearHalvingBlockEntropy h Q 0 ≤ 8 * nearHalvingBlockOutputBits h Q

Total output has at least seven eighths of the initial entropy, without division.