A uniform encoded implementation of the polynomial condenser

For base-field width b = 2 * 3^s and extension degree d = 3^v, the runtime program computes exactly the GUV polynomial map with modulus X^d - t, where t is the named noncube root of the explicit binary field. Source bits are consecutive coefficient blocks, the seed is one binary field element, and the output is the coordinate vector in the same fixed-width representation. Missing source bits are zero and excess bits are ignored.

The equivalence with the larger binary quotient justifies the transpositions around modular squaring. Uniqueness of reduced representatives identifies the intermediate extension polynomial before Horner evaluation. Thus the uniform FP program in Encoding computes the map whose expansion and flat lossless guarantees were proved in the condenser modules. Asymptotic budgets for its unary parameters and the higher extractor construction are separate.

theorem Algebraic.Cutwidth.Extractor.sourcePolynomial_degree_lt (s d : ℕ) (bits : List Bool) : (sourcePolynomial s d bits).degree < ↑d

Interpreting a fixed number of coefficient blocks always gives a bounded-degree source.

theorem Algebraic.Cutwidth.Extractor.sourcePolynomial_inj_of_length (s v n : ℕ) (capacity : n ≤ 2 * 3 ^ s * 3 ^ v) (a b : List Bool) (ha : a.length = n) (hb : b.length = n) (same : sourcePolynomial s (3 ^ v) a = sourcePolynomial s (3 ^ v) b) : a = b

Within capacity, two inputs of the same length encode distinct source polynomials.

theorem Algebraic.Cutwidth.Extractor.sourcePolynomial_injectiveOn_length (s v n : ℕ) (capacity : n ≤ 2 * 3 ^ s * 3 ^ v) : Set.InjOn (sourcePolynomial s (3 ^ v)) {bits : List Bool | bits.length = n}

Padding to the coefficient rectangle preserves every fixed-length input source.

theorem Algebraic.Cutwidth.Extractor.binaryExtensionEquiv_decode_transpose (s v : ℕ) (bits : List Bool) : (binaryExtensionEquiv s v) (BinaryFieldCodec.decode (s + v) (Complexity.BitPolynomial.transposeBits (3 ^ v) (2 * 3 ^ s) bits)) = (AdjoinRoot.mk (extensionModulus s v)) (sourcePolynomial s (3 ^ v) bits)

The bit-matrix transpose is exactly the tower's coefficient-packing map.

theorem Algebraic.Cutwidth.Extractor.decode_blockEvalBits (s : ℕ) (coeffs seed count : List Bool) : BinaryFieldCodec.decode s (Complexity.BitPolynomial.blockEvalBits coeffs (2 * 3 ^ s) seed (Complexity.BitPolynomial.trinomialBits (3 ^ s)) count) = Polynomial.eval (BinaryFieldCodec.decode s seed) (sourcePolynomial s count.length coeffs)

Horner evaluation of arbitrary blocks decodes to source-polynomial evaluation.

theorem Algebraic.Cutwidth.Extractor.sourcePolynomial_unpacked_frobenius (s v : ℕ) (bits count : List Bool) : sourcePolynomial s (3 ^ v) (Complexity.BitPolynomial.transposeBits (2 * 3 ^ s) (3 ^ v) (Complexity.BitPolynomial.frobeniusBits (Complexity.BitPolynomial.transposeBits (3 ^ v) (2 * 3 ^ s) bits) (Complexity.BitPolynomial.trinomialBits (3 ^ (s + v))) count)) = modularFrobenius (extensionModulus s v) count.length (sourcePolynomial s (3 ^ v) bits)

Unpacking the modular binary power recovers the actual reduced extension polynomial.

theorem Algebraic.Cutwidth.Extractor.decode_condenserCoordinateBits (s v : ℕ) (coeffs halfDegree extensionCount seed powerCount : List Bool) (half : halfDegree.length = 3 ^ s) (extension : extensionCount.length = 3 ^ v) : BinaryFieldCodec.decode s (condenserCoordinateBits coeffs halfDegree extensionCount seed powerCount) = Polynomial.eval (BinaryFieldCodec.decode s seed) (modularFrobenius (extensionModulus s v) powerCount.length (sourcePolynomial s (3 ^ v) coeffs))

The computed coordinate is the modular-Frobenius polynomial evaluated at the seed.

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

All decoded output blocks equal the polynomial condenser, in the same coordinate order.

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

The actual paired-input FP evaluator computes the proved polynomial map.

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

Canonically encoding the seed and decoding the output gives the exact polynomial map.