A binomial extension is one larger binary quotient #
Write t for the root of the binary modulus M_s. Adjoining u with
u^(3^v) = t gives the same binary algebra as the quotient by M_(s+v).
The equivalence sends the larger binary root to u; its inverse sends an
embedded base polynomial p(t) to p(u^(3^v)). The polynomial image laws
identify coefficient packing and evaluation in these two representations.
The construction reuses Mathlib's AdjoinRoot.compAlgEquiv, with equality
transports on the supplied defining polynomials:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/AdjoinRoot.html.
Irreducibility uses the binary root's proved noncube property and the Kummer
result documented in Binomial. These are semantic algebraic identifications;
no runtime claim on abstract quotient objects or global field instances is added.
Substitution by a power of three stays within the explicit binary family.
The extension modulus is monic, including its linear case at v = 0.
The extension degree is exactly the selected power of three.
The binary quotient's named noncube root makes the extension irreducible.
The explicit binary quotient and the binomial tower are the same binary algebra.
Equations
Instances For
The larger binary generator maps to the extension generator.
The extension generator maps back to the larger binary generator.
The defining extension relation identifies its generator power with the base root.
The embedded base generator corresponds to the larger generator raised to 3^v.
Every binary polynomial class maps to its evaluation at the extension generator.
Embedded base coefficients evaluate at the corresponding power of the larger root.
An arbitrary extension polynomial evaluates in the larger binary quotient after transporting each coefficient along the same equivalence.