Fixed-width serialization of condenser coordinates

Coordinates are written in increasing index order, each using the canonical binary field width 2 * 3^s. Decoding reads the same consecutive blocks. Zero coordinates give an empty encoding. These semantic codec operations relate coordinate vectors to the runtime program's existing output layout; they introduce no separate runtime algorithm.

noncomputable def Algebraic.Cutwidth.Extractor.encodeCondenserOutput (s m : ℕ) (coords : Fin m → AdjoinRoot (binaryModulus s)) : List Bool

Concatenate the canonical field encodings in coordinate order.

Equations

• Algebraic.Cutwidth.Extractor.encodeCondenserOutput s m coords = (List.ofFn fun (i : Fin m) => Algebraic.Cutwidth.Extractor.BinaryFieldCodec.encode s (coords i)).flatten

noncomputable def Algebraic.Cutwidth.Extractor.decodeCondenserOutput (s m : ℕ) (bits : List Bool) : Fin m → AdjoinRoot (binaryModulus s)

Decode consecutive coordinate blocks; absent input bits use the existing block convention.

Equations

• Algebraic.Cutwidth.Extractor.decodeCondenserOutput s m bits i = Algebraic.Cutwidth.Extractor.BinaryFieldCodec.decode s (Complexity.BitPolynomial.coefficientBlock bits (2 * 3 ^ s) ↑i)