Finite bounds for the rounded near-halving parameters

Under the explicit size guard, the selected schedule accepts source entropy at most 2*b, produces at least b output bits, and pays every split with its actual sparse-field seed width. Its complete seed count, including the final one-shot pair, is at most 2^27 * (Nat.clog 2 (b+1))^3.

These are finite parameter estimates for the recursive method of Chattopadhyay, Goodman, and Liao. The offset and constants account for this library's explicit rounded fields; eventual validity and runtime are separate.

theorem Algebraic.Cutwidth.Extractor.GammaBlockSizeGuard.pos {b : ℕ} (guard : GammaBlockSizeGuard b) : 0 < b

The size guard excludes the empty target.

theorem Algebraic.Cutwidth.Extractor.gammaBlockDepth_le (b : ℕ) : gammaBlockDepth b ≤ gammaBlockLog b

The selected depth is bounded by the input ceiling logarithm.

theorem Algebraic.Cutwidth.Extractor.gammaBlockOutputQuantum_pos (b : ℕ) : 0 < gammaBlockOutputQuantum b

The output quantum is positive even outside the size guard.

theorem Algebraic.Cutwidth.Extractor.gammaBlock_output_ge (b : ℕ) : b ≤ 2 ^ gammaBlockDepth b * gammaBlockLeafLength b

Rounding the reserve upward covers the desired output length.

theorem Algebraic.Cutwidth.Extractor.gammaBlockOutputQuantum_le {b : ℕ} (guard : GammaBlockSizeGuard b) : 2 * gammaBlockOutputQuantum b ≤ b

The rounding quantum consumes at most half of the target length.

theorem Algebraic.Cutwidth.Extractor.gammaBlockInputEntropy_le {b : ℕ} (guard : GammaBlockSizeGuard b) : gammaBlockInputEntropy b ≤ 2 * b

The selected input entropy fits the desired threshold of 2*b bits.

theorem Algebraic.Cutwidth.Extractor.gammaBlockReserve_lower {b : ℕ} (guard : GammaBlockSizeGuard b) : 4096 * (gammaBlockLog b + 1) ^ 2 ≤ gammaBlockReserve b

The reserve pays quadratic logarithmic sparse-field overhead.

theorem Algebraic.Cutwidth.Extractor.gammaBlockReserve_pos {b : ℕ} (guard : GammaBlockSizeGuard b) : 0 < gammaBlockReserve b

The guarded reserve is positive.

theorem Algebraic.Cutwidth.Extractor.gammaBlockBudget_le {b : ℕ} (guard : GammaBlockSizeGuard b) : explicitCondenserBudget (8 * b) (gammaBlockInputEntropy b) (gammaBlockErrorExponent b) ≤ 13 * (gammaBlockLog b + 1)

The common condenser budget is logarithmic in the target length.

theorem Algebraic.Cutwidth.Extractor.gammaBlock_split_budget {b : ℕ} (guard : GammaBlockSizeGuard b) : 12 * (nearHalvingBlockRate (gammaBlockDepth b) + 1) * explicitCondenserBudget (8 * b) (gammaBlockInputEntropy b) (gammaBlockErrorExponent b) + 4 * gammaBlockErrorExponent b ≤ gammaBlockReserve b

The selected reserve satisfies the complete generic split budget.

theorem Algebraic.Cutwidth.Extractor.gammaBlockLeafLength_le {b : ℕ} (guard : GammaBlockSizeGuard b) : gammaBlockLeafLength b ≤ 524296 * (gammaBlockLog b + 1) ^ 3

Each final leaf has a cubic logarithmic output length.

theorem Algebraic.Cutwidth.Extractor.gammaBlockInputEntropy_eq (b : ℕ) : gammaBlockInputEntropy b = nearHalvingBlockEntropy (gammaBlockDepth b) (gammaBlockReserve b) 0

The explicit threshold equals the initial threshold of the generic schedule.

theorem Algebraic.Cutwidth.Extractor.gammaBlockLeafLength_eq (b : ℕ) : gammaBlockLeafLength b = nearHalvingBlockLeafLength (gammaBlockDepth b) (gammaBlockReserve b)

The explicit leaf length equals the generic schedule's final output length.

theorem Algebraic.Cutwidth.Extractor.gammaBlockSeedBits_le {b : ℕ} (guard : GammaBlockSizeGuard b) : nearHalvingBlockSeedBits (8 * b) (gammaBlockDepth b) (gammaBlockReserve b) (gammaBlockErrorExponent b) ≤ 2 ^ 27 * gammaBlockLog b ^ 3

The actual seed count, including both final one-shot seeds, is polylogarithmic.