A sparse binary modulus family

The trinomial X^(2 * 3^s) + X^(3^s) + 1 has a fixed description for every exponent. These are semantic polynomials over ZMod 2; their encoded coefficient vectors and runtime construction are separate definitions.

noncomputable def Algebraic.Cutwidth.Extractor.binaryModulus (s : ℕ) : Polynomial (ZMod 2)

The binary trinomial used for a field of cardinality 2^(2 * 3^s).

Equations

• Algebraic.Cutwidth.Extractor.binaryModulus s = Polynomial.X ^ (2 * 3 ^ s) + Polynomial.X ^ 3 ^ s + 1