Source polynomials represented by binary coefficient blocks

The first d blocks of width 2 * 3^s represent coefficients in the explicit binary quotient. The source polynomial has degree below d; missing input bits are zero, and bits beyond these blocks are ignored. This is the semantic input convention of the runtime condenser, with no source-length promise.

noncomputable def Algebraic.Cutwidth.Extractor.sourcePolynomial (s d : ℕ) (bits : List Bool) : Polynomial (AdjoinRoot (binaryModulus s))

Interpret the first d fixed-width blocks as an extension polynomial.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.decodedCondenser (s : ℕ) (halfDegree extensionCount stride count bits : List Bool) (seed : AdjoinRoot (binaryModulus s)) : Fin count.length → AdjoinRoot (binaryModulus s)

The runtime condenser viewed on semantic field seeds and output coordinates. The seed is encoded at its canonical width before calling the list program.

Equations

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