Output length and uniform polynomial time for one-shot extraction

The selected hash field covers the requested output length. Unary parameter generation composes with the existing condenser and hash certificates to give a single polynomial-time program for all parameters.

theorem Algebraic.Cutwidth.Extractor.Internal.oneShotExtractorBits_length (n ell e : ℕ) (source condenserSeed hashSeed : List Bool) : (oneShotExtractorBits n ell e source condenserSeed hashSeed).length = ell

theorem Algebraic.Cutwidth.Extractor.Internal.oneShotExtractorEval_pair (source condenserSeed hashSeed n ell e : List Bool) : oneShotExtractorEval (Complexity.pair (Complexity.pair source (Complexity.pair condenserSeed hashSeed)) (Complexity.pair n (Complexity.pair ell e))) = oneShotExtractorBits n.length ell.length e.length source condenserSeed hashSeed

theorem Algebraic.Cutwidth.Extractor.Internal.oneShotExtractorEval_length_le (z : List Bool) : (oneShotExtractorEval z).length ≤ z.length

theorem Algebraic.Cutwidth.Extractor.Internal.oneShotExtractorBits_mem_FP {n ell e : List Bool → ℕ} {source condenserSeed hashSeed : List Bool → List Bool} (hn : Complexity.UnaryFn n) (hell : Complexity.UnaryFn ell) (he : Complexity.UnaryFn e) (hsource : source ∈ Complexity.FP) (hcondenser : condenserSeed ∈ Complexity.FP) (hhash : hashSeed ∈ Complexity.FP) : (fun (z : List Bool) => oneShotExtractorBits (n z) (ell z) (e z) (source z) (condenserSeed z) (hashSeed z)) ∈ Complexity.FP

theorem Algebraic.Cutwidth.Extractor.Internal.oneShotExtractorEval_mem_FP : oneShotExtractorEval ∈ Complexity.FP