Total polynomial-time evaluation of the Gamma runtime

The size guard selects a certified full run or a zero-step run. Both branches therefore satisfy the loop's resource contract before the final conditional output is selected. Unconditional parameter generation and bounded powering give one FP program; the statistical size guard is not an FP premise.

theorem Algebraic.Cutwidth.Extractor.Internal.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)

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

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

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

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

theorem Algebraic.Cutwidth.Extractor.Internal.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

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