Runtime binary program for polynomial condensation

Source coefficients are consecutive blocks of width twice the half-degree word's length. Transposition packs them for modular Frobenius iteration; the inverse transposition restores the blocks for evaluation at the seed. Every dimension and iteration count is supplied at runtime as a word length.

The output concatenates fixed-width coordinates without list framing. These are total list programs, including zero dimensions and malformed paired inputs. Their interpretation in finite fields is a separate correctness theorem requiring the intended powers-of-three dimensions.

def Algebraic.Cutwidth.Extractor.condenserCoordinateBits (coeffs halfDegree extensionCount seed powerCount : List Bool) : List Bool

One condenser coordinate, with a runtime number of modular squarings.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Cutwidth.Extractor.condenserBits (coeffs halfDegree extensionCount seed stride count : List Bool) : List Bool

Consecutive coordinates use stride.length * i modular squarings.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Cutwidth.Extractor.condenserEval (z : List Bool) : List Bool

Runtime codec: pair (pair (pair coeffs halfDegree) (pair extensionCount seed)) (pair stride count). The result contains coordinate bits, without the seed.

Equations

• One or more equations did not get rendered due to their size.