Logarithmic depth selection and ceiling-reserve estimates

Exact power bounds from the size guard control both the reserve and the output rounding quantum. The reserve pays the full sparse-field width; the final seed estimate includes the one-shot pair shared by all leaves. The offset and constants are deductions for this library's rounded fields.

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

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

theorem Algebraic.Cutwidth.Extractor.Internal.gammaBlock_power_lower {b : ℕ} (guard : GammaBlockSizeGuard b) : 2 ^ gammaBlockDepth b * 32768 * (gammaBlockLog b + 1) ^ 3 ≤ b

theorem Algebraic.Cutwidth.Extractor.Internal.gammaBlock_power_upper {b : ℕ} (guard : GammaBlockSizeGuard b) : b < 2 ^ gammaBlockDepth b * 524288 * (gammaBlockLog b + 1) ^ 3

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

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

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

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

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

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

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

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

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

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

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

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