A uniform runtime program for polynomial condensation

One polynomial-time evaluator handles all coefficient lists, seeds, unary dimensions, and iteration counts. Its output concatenates fixed-width coordinates, which can be recovered by taking consecutive blocks.

The results here describe the total program and its resource bound. They impose no field or irreducibility assumptions; the finite-field meaning of the generated trinomials and packed arithmetic is proved separately.

theorem Algebraic.Cutwidth.Extractor.condenserCoordinateBits_length (coeffs halfDegree extensionCount seed powerCount : List Bool) : (condenserCoordinateBits coeffs halfDegree extensionCount seed powerCount).length = 2 * halfDegree.length

Each coordinate has the requested coefficient width, including width zero.

theorem Algebraic.Cutwidth.Extractor.condenserBits_length (coeffs halfDegree extensionCount seed stride count : List Bool) : (condenserBits coeffs halfDegree extensionCount seed stride count).length = count.length * (2 * halfDegree.length)

The output contains exactly the requested number of fixed-width coordinates.

theorem Algebraic.Cutwidth.Extractor.coefficientBlock_condenserBits (coeffs halfDegree extensionCount seed stride count : List Bool) (i : ℕ) (hi : i < count.length) : Complexity.BitPolynomial.coefficientBlock (condenserBits coeffs halfDegree extensionCount seed stride count) (2 * halfDegree.length) i = condenserCoordinateBits coeffs halfDegree extensionCount seed (List.replicate (stride.length * i) true)

Taking the ith output block recovers the coordinate with stride.length * i modular squarings.

theorem Algebraic.Cutwidth.Extractor.condenserEval_pair (coeffs halfDegree extensionCount seed stride count : List Bool) : condenserEval (Complexity.pair (Complexity.pair (Complexity.pair coeffs halfDegree) (Complexity.pair extensionCount seed)) (Complexity.pair stride count)) = condenserBits coeffs halfDegree extensionCount seed stride count

The paired evaluator implements the six-argument list program.

theorem Algebraic.Cutwidth.Extractor.condenserEval_length_le (z : List Bool) : (condenserEval z).length ≤ 2 * z.length ^ 2

Even malformed paired inputs have a quadratic output-length bound.

theorem Algebraic.Cutwidth.Extractor.condenserCoordinateBits_mem_FP {coeffs halfDegree extensionCount seed powerCount : List Bool → List Bool} (hcoeffs : coeffs ∈ Complexity.FP) (hhalfDegree : halfDegree ∈ Complexity.FP) (hextensionCount : extensionCount ∈ Complexity.FP) (hseed : seed ∈ Complexity.FP) (hpowerCount : powerCount ∈ Complexity.FP) : (fun (z : List Bool) => condenserCoordinateBits (coeffs z) (halfDegree z) (extensionCount z) (seed z) (powerCount z)) ∈ Complexity.FP

One coordinate is uniformly polynomial-time for polynomial-time runtime operands.

theorem Algebraic.Cutwidth.Extractor.condenserBits_mem_FP {coeffs halfDegree extensionCount seed stride count : List Bool → List Bool} (hcoeffs : coeffs ∈ Complexity.FP) (hhalfDegree : halfDegree ∈ Complexity.FP) (hextensionCount : extensionCount ∈ Complexity.FP) (hseed : seed ∈ Complexity.FP) (hstride : stride ∈ Complexity.FP) (hcount : count ∈ Complexity.FP) : (fun (z : List Bool) => condenserBits (coeffs z) (halfDegree z) (extensionCount z) (seed z) (stride z) (count z)) ∈ Complexity.FP

The coordinate concatenation is uniformly polynomial-time in all runtime operands.

theorem Algebraic.Cutwidth.Extractor.condenserEval_mem_FP : condenserEval ∈ Complexity.FP

A single polynomial-time machine computes the paired runtime condenser program.