Uniform polynomial-time condense-then-hash extraction

The total program emits exactly ell bits for every input and every pair of seed words. Its parameter generation and runtime belong to FP uniformly in unary n, ell, and e. Correctness identifies the program with the linear statistical map; OneShot.Extraction supplies the retained-seed error bound on fixed-length flat sources.

This is one round of condensation and hashing. Its finite seed bound depends on the output length as well as source length and error; it does not yet provide the recursive seed reuse needed for the final hard family.

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

The selected field always produces exactly the requested number of output bits.

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

The paired evaluator reads source, seeds, and three unary parameters.

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

Every paired input, including malformed encodings, bounds its output length.

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

Condensation and hashing are uniformly polynomial-time with unary parameters.

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

A single polynomial-time evaluator computes the extractor at all unary parameters.