Irreducible binomial moduli from one noncube coefficient

Every noncube a gives the monic irreducible modulus X^(3^s) - a of exact degree 3^s, including s = 0. Such coefficients exist in every finite field whose multiplicative-group order is divisible by three.

Irreducibility reuses Mathlib's X_pow_sub_C_irreducible_of_prime_pow_of_ne_two, formalized by Andrew Yang and Patrick Lutz in Mathlib.FieldTheory.KummerExtension: https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/KummerExtension.html. Noncube existence uses Cauchy's finite-group theorem, Mathlib's Fintype.card_units, and equivalence of injectivity and surjectivity on a finite type. This layer supplies no encoded selection algorithm or runtime claim; the field, coefficient, and exponent remain parameters.

theorem Algebraic.Cutwidth.Extractor.binomialModulus_monic {F : Type u_1} [Ring F] (a : F) (s : ℕ) : (binomialModulus a s).Monic

The leading coefficient is one for every coefficient and exponent.

theorem Algebraic.Cutwidth.Extractor.binomialModulus_natDegree {F : Type u_1} [Ring F] [Nontrivial F] (a : F) (s : ℕ) : (binomialModulus a s).natDegree = 3 ^ s

The degree is exactly 3^s, including degree one at s = 0.

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

A noncube coefficient makes every member of the binomial family irreducible.

theorem Algebraic.Cutwidth.Extractor.exists_noncube {F : Type u_1} [Field F] [Fintype F] (divisible : 3 ∣ Fintype.card F - 1) : ∃ (a : F), ∀ (b : F), b ^ 3 ≠ a

Divisibility of the multiplicative-group order guarantees a noncube.

theorem Algebraic.Cutwidth.Extractor.three_dvd_card_sub_one_of_even_exponent {F : Type u_1} [Fintype F] {b : ℕ} (cardinality : Fintype.card F = 2 ^ b) (even : Even b) : 3 ∣ Fintype.card F - 1

A binary field cardinality with even exponent has unit-group order divisible by three. Only the cardinality identity is needed for this arithmetic fact.

theorem Algebraic.Cutwidth.Extractor.binomialModulus_natDegree_clog_bounds {F : Type u_1} [Ring F] [Nontrivial F] (a : F) {n : ℕ} (positive : 0 < n) : n ≤ (binomialModulus a (Nat.clog 3 n)).natDegree ∧ (binomialModulus a (Nat.clog 3 n)).natDegree < 3 * n

Rounding a positive target degree up to a power of three increases it by less than a factor of three.