The sparse binary trinomial modulus #

The monic irreducible trinomial X^(2 * 3^s) + X^(3^s) + 1 defines a binary field of cardinality 2^(2 * 3^s). Its named quotient root is a noncube, so it can supply the next binomial modulus coefficient without an existence choice.

Irreducibility uses Mathlib's Polynomial.irreducible_comp, the four-element field generated by the base quadratic, and the Kummer theorem documented in Binomial. The root's noncube property follows from the irreducibility of the next trinomial and Mathlib's finite-module minimal-polynomial degree bound: https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/Minpoly/Finite.html. These are semantic algebraic facts. Binary.Codec supplies the fixed-width quotient representation, and Binary.Encoding connects a uniform modulus generator and modular-squaring program. Binary.Extension identifies the larger quotient used by the complete evaluator in Condenser.Encoding.Correctness.

source

theorem Algebraic.Cutwidth.Extractor.binaryModulus_monic (s : ℕ) :

(binaryModulus s).Monic

Every binary trinomial in the family is monic.

source

theorem Algebraic.Cutwidth.Extractor.binaryModulus_natDegree (s : ℕ) :

(binaryModulus s).natDegree = 2 * 3 ^ s

The leading exponent gives the exact degree.

source

theorem Algebraic.Cutwidth.Extractor.binaryModulus_irreducible (s : ℕ) :

Irreducible (binaryModulus s)

Composing the irreducible base quadratic with a power of three preserves irreducibility because its generator is a noncube in the four-element field.