Total unary computation of the rounded Gamma parameters

The selected depth never exceeds the binary floor logarithm. Its power of two therefore fits the unary bound b+1, even when the size guard fails. Bounded powering and arithmetic certify every parameter without a promise.

theorem Algebraic.Cutwidth.Extractor.Internal.gammaBlockDepth_pow_le (b : ℕ) : 2 ^ gammaBlockDepth b ≤ b + 1

theorem Algebraic.Cutwidth.Extractor.Internal.gammaBlockLog_unaryFn {b : List Bool → ℕ} (hb : Complexity.UnaryFn b) : Complexity.UnaryFn fun (z : List Bool) => gammaBlockLog (b z)

theorem Algebraic.Cutwidth.Extractor.Internal.gammaBlockDepth_unaryFn {b : List Bool → ℕ} (hb : Complexity.UnaryFn b) : Complexity.UnaryFn fun (z : List Bool) => gammaBlockDepth (b z)

theorem Algebraic.Cutwidth.Extractor.Internal.gammaBlockDepth_pow_unaryFn {b : List Bool → ℕ} (hb : Complexity.UnaryFn b) : Complexity.UnaryFn fun (z : List Bool) => 2 ^ gammaBlockDepth (b z)

theorem Algebraic.Cutwidth.Extractor.Internal.gammaBlockErrorExponent_unaryFn {b : List Bool → ℕ} (hb : Complexity.UnaryFn b) : Complexity.UnaryFn fun (z : List Bool) => gammaBlockErrorExponent (b z)

theorem Algebraic.Cutwidth.Extractor.Internal.gammaBlockOutputQuantum_unaryFn {b : List Bool → ℕ} (hb : Complexity.UnaryFn b) : Complexity.UnaryFn fun (z : List Bool) => gammaBlockOutputQuantum (b z)

theorem Algebraic.Cutwidth.Extractor.Internal.gammaBlockReserve_unaryFn {b : List Bool → ℕ} (hb : Complexity.UnaryFn b) : Complexity.UnaryFn fun (z : List Bool) => gammaBlockReserve (b z)

theorem Algebraic.Cutwidth.Extractor.Internal.gammaBlockLeafLength_unaryFn {b : List Bool → ℕ} (hb : Complexity.UnaryFn b) : Complexity.UnaryFn fun (z : List Bool) => gammaBlockLeafLength (b z)

theorem Algebraic.Cutwidth.Extractor.Internal.gammaBlockInputEntropy_unaryFn {b : List Bool → ℕ} (hb : Complexity.UnaryFn b) : Complexity.UnaryFn fun (z : List Bool) => gammaBlockInputEntropy (b z)

theorem Algebraic.Cutwidth.Extractor.Internal.gammaBlockSizeGuard_fpPred {b : List Bool → ℕ} (hb : Complexity.UnaryFn b) : Complexity.FPPred fun (z : List Bool) => GammaBlockSizeGuard (b z)

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlockRate_unaryFn {h : List Bool → ℕ} (hh : Complexity.UnaryFn h) : Complexity.UnaryFn fun (z : List Bool) => nearHalvingBlockRate (h z)