A uniform total program for the rounded Gamma family

The runtime generates the rounded parameters, executes the certified number of near-halving levels, and returns exactly the requested output width. It is polynomial-time on all source and seed words, including inputs outside the statistical size guard. The paired evaluator infers the target width as the decoded source length divided by eight.

These are program and resource statements. Agreement with the semantic extractor on canonical seeds is proved in the correctness layer.

theorem Algebraic.Cutwidth.Extractor.gammaBlockExtractorRuntime_of_guard (b : ℕ) (source seeds : List Bool) (guard : GammaBlockSizeGuard b) : gammaBlockExtractorRuntime b source seeds = List.take b (nearHalvingBlockExtractorBits (8 * b) (gammaBlockDepth b) (gammaBlockReserve b) (gammaBlockErrorExponent b) (gammaBlockLeafLength b) (gammaBlockDepth b) source seeds)

On the size guard, run the selected depth and retain the requested output prefix.

theorem Algebraic.Cutwidth.Extractor.gammaBlockExtractorRuntime_of_not_guard (b : ℕ) (source seeds : List Bool) (guard : ¬GammaBlockSizeGuard b) : gammaBlockExtractorRuntime b source seeds = List.replicate b false

Outside the size guard, the total runtime emits an all-false word.

theorem Algebraic.Cutwidth.Extractor.gammaBlockExtractorRuntime_length (b : ℕ) (source seeds : List Bool) : (gammaBlockExtractorRuntime b source seeds).length = b

Every source and seed word yields exactly the requested number of output bits.

theorem Algebraic.Cutwidth.Extractor.gammaBlockExtractorEval_pair (source seeds : List Bool) : gammaBlockExtractorEval (Complexity.pair source seeds) = gammaBlockExtractorRuntime (source.length / 8) source seeds

The paired evaluator decodes its source and seed words before inferring the width.

theorem Algebraic.Cutwidth.Extractor.gammaBlockExtractorEval_length (z : List Bool) : (gammaBlockExtractorEval z).length = (Complexity.pairFst z).length / 8

Arbitrary encoded words have the output width determined by their decoded source.

theorem Algebraic.Cutwidth.Extractor.gammaBlockExtractorRuntime_mem_FP {b : List Bool → ℕ} {source seeds : List Bool → List Bool} (hb : Complexity.UnaryFn b) (hsource : source ∈ Complexity.FP) (hseeds : seeds ∈ Complexity.FP) : (fun (z : List Bool) => gammaBlockExtractorRuntime (b z) (source z) (seeds z)) ∈ Complexity.FP

The total runtime is polynomial-time in its unary width and two runtime words.

theorem Algebraic.Cutwidth.Extractor.gammaBlockExtractorEval_mem_FP : gammaBlockExtractorEval ∈ Complexity.FP

One polynomial-time program evaluates the family on every encoded input word.