Fixed-width semantic representations of binary quotient elements

Decoding interprets low-to-high coefficient bits and takes their quotient class. Encoding reads the coefficients of the unique remainder of degree below the binary modulus, retaining exactly 2 * 3^s bits. These functions relate the semantic quotient to bit lists; they assert no runtime bound on abstract quotient objects and introduce no global field or finiteness instances.

@[reducible, inline]

abbrev Algebraic.Cutwidth.Extractor.BinaryFieldCodec.Bits (s : ℕ) : Type

Canonical-width coefficient lists for the sth binary quotient.

Equations

• Algebraic.Cutwidth.Extractor.BinaryFieldCodec.Bits s = { bits : List Bool // bits.length = 2 * 3 ^ s }

noncomputable def Algebraic.Cutwidth.Extractor.BinaryFieldCodec.decode (s : ℕ) (bits : List Bool) : AdjoinRoot (binaryModulus s)

Interpret a coefficient list and then pass to its binary quotient class.

Equations

• Algebraic.Cutwidth.Extractor.BinaryFieldCodec.decode s bits = (AdjoinRoot.mk (Algebraic.Cutwidth.Extractor.binaryModulus s)) (Complexity.BitPolynomial.ofBits bits)

noncomputable def Algebraic.Cutwidth.Extractor.BinaryFieldCodec.encode (s : ℕ) (x : AdjoinRoot (binaryModulus s)) : List Bool

Read every coefficient below the modulus degree, retaining high zero bits.

Equations

• Algebraic.Cutwidth.Extractor.BinaryFieldCodec.encode s x = List.ofFn fun (i : Fin (2 * 3 ^ s)) => decide (((AdjoinRoot.modByMonicHom ⋯) x).coeff ↑i = 1)