The complete runtime program implements the polynomial condenser

Each fixed-width output block is the corresponding modular-Frobenius coordinate evaluated at the seed. Concatenation preserves their order, and the total paired-input evaluator agrees with this same list program.

theorem Algebraic.Cutwidth.Extractor.Internal.condenserBits_correct (s v : ℕ) (coeffs halfDegree extensionCount seed stride count : List Bool) (half : halfDegree.length = 3 ^ s) (extension : extensionCount.length = 3 ^ v) : (fun (i : Fin count.length) => BinaryFieldCodec.decode s (Complexity.BitPolynomial.coefficientBlock (condenserBits coeffs halfDegree extensionCount seed stride count) (2 * 3 ^ s) ↑i)) = polynomialCondenser (extensionModulus s v) stride.length count.length (sourcePolynomial s (3 ^ v) coeffs) (BinaryFieldCodec.decode s seed)

theorem Algebraic.Cutwidth.Extractor.Internal.condenserEval_correct (s v : ℕ) (coeffs halfDegree extensionCount seed stride count : List Bool) (half : halfDegree.length = 3 ^ s) (extension : extensionCount.length = 3 ^ v) : (fun (i : Fin count.length) => BinaryFieldCodec.decode s (Complexity.BitPolynomial.coefficientBlock (condenserEval (Complexity.pair (Complexity.pair (Complexity.pair coeffs halfDegree) (Complexity.pair extensionCount seed)) (Complexity.pair stride count))) (2 * 3 ^ s) ↑i)) = polynomialCondenser (extensionModulus s v) stride.length count.length (sourcePolynomial s (3 ^ v) coeffs) (BinaryFieldCodec.decode s seed)

theorem Algebraic.Cutwidth.Extractor.Internal.decodedCondenser_eq (s v : ℕ) (halfDegree extensionCount stride count bits : List Bool) (seed : AdjoinRoot (binaryModulus s)) (half : halfDegree.length = 3 ^ s) (extension : extensionCount.length = 3 ^ v) : decodedCondenser s halfDegree extensionCount stride count bits seed = polynomialCondenser (extensionModulus s v) stride.length count.length (sourcePolynomial s (3 ^ v) bits) seed