An explicit finite reserve for constant-rate block recursion

The reserve 4096*(L+E+1) controls the initial rate-one compression and pays for the later rate-three split budgets. The initial output width is between the initial entropy and sixty-four times that entropy. Its condenser budget is bounded by E+4*h+2*clog 2 (L+E+1)+64, retaining logarithmic dependence on the reserve instead of charging its full size to every seed.

These estimates are our arithmetic deductions from the checked sparse-field rate bounds. The recursive condensation and splitting method is credited in Recursion.Extraction. This module proves finite inequalities only; the recurrence, its total seed cost, and an encoded evaluator are separate layers.

theorem Algebraic.Cutwidth.Extractor.recursiveBlockReserve_pos (L E : ℕ) : 0 < recursiveBlockReserve L E

The explicit reserve is positive for every pair of natural parameters.

theorem Algebraic.Cutwidth.Extractor.recursiveBlockEntropy_zero_clog_le (L E h : ℕ) : Nat.clog 2 (recursiveBlockEntropy h (recursiveBlockReserve L E) 0 + 1) ≤ 2 * h + 13 + Nat.clog 2 (L + E + 1)

The initial entropy has a logarithm linear in depth and logarithmic in the reserve.

theorem Algebraic.Cutwidth.Extractor.recursiveBlockInitialWidth_bounds (n L E h : ℕ) (length : Nat.clog 2 (n + 1) ≤ L) : have Q := recursiveBlockReserve L E; have k := recursiveBlockEntropy h Q 0; have N := explicitCondenserHalfWidth n k E 1 + explicitCondenserHalfWidth n k E 1; k ≤ N ∧ N ≤ 64 * k

Initial rate-one compression preserves capacity and has bounded expansion.

theorem Algebraic.Cutwidth.Extractor.recursiveBlockInitialBudget_le (n L E h : ℕ) (length : Nat.clog 2 (n + 1) ≤ L) : have Q := recursiveBlockReserve L E; have k := recursiveBlockEntropy h Q 0; have N := explicitCondenserHalfWidth n k E 1 + explicitCondenserHalfWidth n k E 1; explicitCondenserBudget N k E ≤ E + 4 * h + 2 * Nat.clog 2 (L + E + 1) + 64

The largest later budget depends on the logarithm of the initial compressed width.

theorem Algebraic.Cutwidth.Extractor.recursiveBlockReserve_budget (n L E h : ℕ) (length : Nat.clog 2 (n + 1) ≤ L) (depth : h ≤ L) : have Q := recursiveBlockReserve L E; have k := recursiveBlockEntropy h Q 0; have N := explicitCondenserHalfWidth n k E 1 + explicitCondenserHalfWidth n k E 1; 3 * (24 * explicitCondenserBudget N k E) + 6 * E ≤ 2 * Q

The reserve pays the uniform field-width and split-error slack for rate three.