Uniform binary condensation with an explicit parameter schedule

One polynomial-time program computes the field dimensions, extension degree, powering stride, coordinate count, and output from four unary parameters and two input words. Its decoded coordinates are exactly the previously proved polynomial condenser, and it preserves source XOR for each fixed seed.

The output length satisfies the exact rate bound u*length ≤ (u+1)*k + u*b. The seed width b is bounded in Parameters.Explicit; the finite statistical guarantees for this same program are in Encoding.Explicit.Lossless. The underlying polynomial map and sparse-parameter source credits are recorded in Condenser.Polynomial and Parameters.Sparse.

theorem Algebraic.Cutwidth.Extractor.explicitCondenserBits_length (n k e u : ℕ) (source seed : List Bool) : (explicitCondenserBits n k e u source seed).length = condenserCoordinates k (sparsePowerBits u (explicitCondenserBudget n k e)) * sparseFieldBits u (explicitCondenserBudget n k e)

The output has one fixed-width block per selected coordinate.

theorem Algebraic.Cutwidth.Extractor.explicitCondenserBits_output_rate (n k e u : ℕ) (source seed : List Bool) : u * (explicitCondenserBits n k e u source seed).length ≤ (u + 1) * k + u * sparseFieldBits u (explicitCondenserBudget n k e)

The actual program's output satisfies the selected rate bound.

theorem Algebraic.Cutwidth.Extractor.explicitCondenserEval_pair (source seed n k e u : List Bool) : explicitCondenserEval (Complexity.pair (Complexity.pair source seed) (Complexity.pair (Complexity.pair n k) (Complexity.pair e u))) = explicitCondenserBits n.length k.length e.length u.length source seed

The paired evaluator reads all four numerical parameters from word lengths.

theorem Algebraic.Cutwidth.Extractor.decodedExplicitCondenser_eq (n k e u : ℕ) (bits : List Bool) (seed : AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e)))) : let T := explicitCondenserBudget n k e; let s := sparseFieldExponent u T; have v := explicitCondenserExtensionExponent n k e u; let r := sparsePowerBits u T; let m := condenserCoordinates k r; decodedExplicitCondenser n k e u bits seed = polynomialCondenser (extensionModulus s v) r m (sourcePolynomial s (explicitCondenserExtensionDegree n k e u) bits) seed

The scheduled program computes the exact polynomial condenser at its selected parameters.

theorem Algebraic.Cutwidth.Extractor.decodedExplicitCondenser_addBits (n k e u : ℕ) (a b : List Bool) (seed : AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e)))) : decodedExplicitCondenser n k e u (Complexity.BitPolynomial.addBits a b) seed = decodedExplicitCondenser n k e u a seed + decodedExplicitCondenser n k e u b seed

For every field seed, the actual scheduled output preserves padded source XOR.

theorem Algebraic.Cutwidth.Extractor.decodedExplicitCondenser_replicate_false (n k e u length : ℕ) (seed : AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e)))) : decodedExplicitCondenser n k e u (List.replicate length false) seed = 0

Every all-false source produces the zero coordinate vector.

theorem Algebraic.Cutwidth.Extractor.explicitCondenserBits_mem_FP {n k e u : List Bool → ℕ} {source seed : List Bool → List Bool} (hn : Complexity.UnaryFn n) (hk : Complexity.UnaryFn k) (he : Complexity.UnaryFn e) (hu : Complexity.UnaryFn u) (hsource : source ∈ Complexity.FP) (hseed : seed ∈ Complexity.FP) : (fun (z : List Bool) => explicitCondenserBits (n z) (k z) (e z) (u z) (source z) (seed z)) ∈ Complexity.FP

Uniform polynomial time includes parameter generation, with every operand variable.

theorem Algebraic.Cutwidth.Extractor.explicitCondenserEval_mem_FP : explicitCondenserEval ∈ Complexity.FP

A single polynomial-time machine computes the complete paired program.