The binomial quotient supplies the next noncube coefficient

The adjoined root of X^(3^s) - a has norm a. If a is a noncube, norm multiplicativity shows that the root is also a noncube. It therefore gives another monic irreducible binomial of every power-of-three degree.

The norm computation reuses Mathlib's power-basis norm formula Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly and its monic AdjoinRoot power basis: https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Norm/Basic.html. The next irreducibility step uses the Kummer theorem documented in Binomial. These are semantic algebraic facts about supplied data; no encoded field representation, coefficient-selection algorithm, or runtime bound is asserted.

theorem Algebraic.Cutwidth.Extractor.norm_root_binomialModulus {F : Type u_1} [Field F] (a : F) (s : ℕ) : (Algebra.norm F) (AdjoinRoot.root (binomialModulus a s)) = a

Odd degree makes the quotient root's norm equal to the supplied coefficient. This identity does not require irreducibility.

theorem Algebraic.Cutwidth.Extractor.root_binomialModulus_noncube {F : Type u_1} [Field F] (a : F) (s : ℕ) (noncube : ∀ (b : F), b ^ 3 ≠ a) (b : AdjoinRoot (binomialModulus a s)) : b ^ 3 ≠ AdjoinRoot.root (binomialModulus a s)

A cube root of the adjoined root would have norm a cube root of a.

theorem Algebraic.Cutwidth.Extractor.binomialModulus_root_properties {F : Type u_1} [Field F] (a : F) (s v : ℕ) (noncube : ∀ (b : F), b ^ 3 ≠ a) : (binomialModulus (AdjoinRoot.root (binomialModulus a s)) v).Monic ∧ Irreducible (binomialModulus (AdjoinRoot.root (binomialModulus a s)) v) ∧ (binomialModulus (AdjoinRoot.root (binomialModulus a s)) v).natDegree = 3 ^ v

The first quotient's root supplies the coefficient of a second monic irreducible binomial, with exact degree 3^v. Both exponents may be zero.