Uniform unary generation of the rounded Gamma parameters

Every selected parameter is polynomial-time in its unary input, including the actual block count 2^depth. The unconditional bound 2^depth <= b+1 permits bounded powering on all inputs. The size guard also has a polynomial-time decision algorithm; none of these certificates assumes it.

These statements generate parameters. They do not certify a recursive extractor evaluator or generate its recursively varying total seed length.

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

The selected block count has a unary bound on every input.

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

The ceiling input logarithm can be generated in unary in polynomial time.

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

The total depth formula uses polynomial-time logarithms and subtraction.

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

The actual block count is polynomial-time by bounded powering.

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

The common error exponent is polynomial-time in unary.

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

The complete output quantum is polynomial-time in unary.

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

Ceiling division generates the selected reserve on all inputs.

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

The final leaf output length is polynomial-time in unary.

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

The actual selected input entropy is polynomial-time in unary.

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

The size guard has a total polynomial-time decision algorithm.

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

The rate required by the near-halving schedule is polynomial-time in unary.