Finite reserve and resource bounds for the near-halving schedule

The exact entropy gap pays the full rounded field width and the splitting error. Induction bounds every actual block by the initial width, allowing one logarithmic budget to control all levels. The final seed pair is included in the resource bound, with its one-step larger condenser error exponent.

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

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

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

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlock_split_numeric (h Q B E : ℕ) (reserve : 2 * (B + 2 * E) ≤ Q) {i : ℕ} (level : i < h) : nearHalvingBlockRate h * (B + 2 * (nearHalvingBlockEntropy h Q (i + 1) + E)) ≤ (nearHalvingBlockRate h - 1) * nearHalvingBlockEntropy h Q i

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlockSeedWidth_le_of_width (N h Q E i : ℕ) (bounded : nearHalvingBlockWidth N h Q E i ≤ N) : nearHalvingBlockSeedWidth N h Q E i ≤ 6 * (nearHalvingBlockRate h + 1) * explicitCondenserBudget N (nearHalvingBlockEntropy h Q 0) E

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlock_step (N h Q E : ℕ) (reserve : 2 * (6 * (nearHalvingBlockRate h + 1) * explicitCondenserBudget N (nearHalvingBlockEntropy h Q 0) E + 2 * E) ≤ Q) {i : ℕ} (level : i < h) (bounded : nearHalvingBlockWidth N h Q E i ≤ N) : 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

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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

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

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

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

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlock_seed_sum_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) : (Finset.range h).sum (nearHalvingBlockSeedWidth N h Q E) ≤ h * (6 * (nearHalvingBlockRate h + 1) * explicitCondenserBudget N (nearHalvingBlockEntropy h Q 0) E)

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

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

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

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlock_leaf_seed_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) : have ell := nearHalvingBlockLeafLength h Q; 2 * 3 ^ oneShotCondenserExponent (nearHalvingBlockWidth N h Q E h) ell E + 2 * 3 ^ oneShotHashExponent (nearHalvingBlockWidth N h Q E h) ell E ≤ 84 * (explicitCondenserBudget N (nearHalvingBlockEntropy h Q 0) E + 1) + 18 * ell + 24 * E + 6

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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)