Binary quotient size and the noncube root

The monic power basis gives the quotient cardinality. Cubing in the defining polynomial passes from M_s to M_(s+1). A cube root of the quotient root would therefore have minimal polynomial degree larger than the quotient's dimension, contradicting the finite-module degree bound.

theorem Algebraic.Cutwidth.Extractor.Internal.card_adjoinRoot_binaryModulus (s : ℕ) : Nat.card (AdjoinRoot (binaryModulus s)) = 2 ^ (2 * 3 ^ s)

theorem Algebraic.Cutwidth.Extractor.Internal.binaryModulus_comp_cube (s : ℕ) : (binaryModulus s).comp (Polynomial.X ^ 3) = binaryModulus (s + 1)

theorem Algebraic.Cutwidth.Extractor.Internal.root_binaryModulus_noncube (s : ℕ) (b : AdjoinRoot (binaryModulus s)) : b ^ 3 ≠ AdjoinRoot.root (binaryModulus s)