Irreducibility of X^6 + X^3 + 1 over KoalaBear

The sextic X^6 + X^3 + 1 is the ninth cyclotomic polynomial Φ₉, so it is irreducible over KoalaBear.Field exactly because p has multiplicative order 6 modulo 9 (p ≡ 2 mod 9); its root is a primitive 9th root of unity. It is the defining polynomial of the degree-6 extension in CompPoly/Fields/KoalaBear/Ext6.lean.

No degree-6 binomial does the job, for the same reason as at degree 5 but one step stronger: p - 1 = 2^24 · 127, so 3 ∤ p - 1, x ↦ x^3 is a bijection on KoalaBear, and every W is a cube V^3 — whence X^6 - W = (X^2 - V)(X^4 + V X^2 + V^2) factors for every W.

Φ₉ is chosen among the irreducible sextics for arithmetic reasons. Every entry of the reduction table X^6 … X^10 mod f is ±1, so reduction costs no base-field multiplications, and the same holds for the Frobenius matrix (θ ↦ θ^2, since p ≡ 2 mod 9). It also exposes the 2-then-3 tower for free: θ^3 is a primitive cube root of unity, and F_p(θ^3) = F_p² because Y^2 + Y + 1 is irreducible over KoalaBear.

Certificates

Degree 6 is composite, so Rabin's test needs the trace condition plus one coprimality check per prime factor of 6 — at p^3 (for ℓ = 2) and p^2 (for ℓ = 3). The collapsed prime-degree form is not just weaker but unsound here: (X^3 + X + 4)(X^3 + X - 4) divides X^(p^6) - X and is coprime to X^p - X, so it would pass. The three conditions are discharged by kernel-checked certificates from CompPoly/Fields/KoalaBear/Ext6/SexticCertData.lean (generated by scripts/gen_rabin_certificate.py): a 258-step chain for the trace, 121 and 75 steps plus a Bézout identity for the two coprimality checks. Each chain is verified by a single kernel reduction of CompPoly.RabinCert.runChain — Nat arithmetic only, no native_decide.

Main statements

• KoalaBear.sexticPoly: the polynomial X^6 + X^3 + 1 over KoalaBear.Field.
• KoalaBear.sexticPoly_irreducible, and the Fact instance consumed by CompPoly.Extension.Ext.instField.

noncomputable def KoalaBear.sexticPoly : Polynomial Field

The defining sextic X^6 + X^3 + 1 = Φ₉ of the degree-6 KoalaBear extension.

def KoalaBear.sexticL : List ℕ

The sextic's little-endian ℕ-coefficient encoding. Every coefficient of Φ₉ is 0 or 1, so unlike the quintic this needs no p - 1 literal to spell a negative coefficient.

theorem KoalaBear.toPoly_sexticL : CompPoly.RabinCert.toPoly fieldSize sexticL = sexticPoly

The ℕ-coefficient encoding denotes the sextic.

theorem KoalaBear.sexticPoly_natDegree : sexticPoly.natDegree = 6

theorem KoalaBear.sexticPoly_ne_zero : sexticPoly ≠ 0

The kernel-checked certificates

Each theorem below is one kernel reduction: runChain re-verifies every step of the generated chain (cur² = q·f + r, coefficientwise mod p), and chainExp recomputes the exponent the chain reaches. eqModP checks the Bézout identities for coprimality.

theorem KoalaBear.sextic_trace_chain : CompPoly.RabinCert.runChain fieldSize sexticL [0, 1] SexticCert.traceSteps = some [0, 1]

The 258-step chain for X^(p^6) mod f verifies and ends at the residue X.

theorem KoalaBear.sextic_trace_exp : CompPoly.RabinCert.chainExp 1 SexticCert.traceSteps = fieldSize ^ 6

The trace chain computes the exponent p^6.

Coprimality with X^(p^3) - X, the check for the prime factor 2 of 6

theorem KoalaBear.sextic_cop3_chain : CompPoly.RabinCert.runChain fieldSize sexticL [0, 1] SexticCert.cop3Steps = some SexticCert.cop3Rp

The 121-step chain for X^(p^3) mod f verifies and ends at the recorded residue.

theorem KoalaBear.sextic_cop3_exp : CompPoly.RabinCert.chainExp 1 SexticCert.cop3Steps = fieldSize ^ 3

The chain computes the exponent p^3.

theorem KoalaBear.sextic_cop3_w_check : CompPoly.RabinCert.eqModP fieldSize SexticCert.cop3Rp (CompPoly.RabinCert.addNat SexticCert.cop3W [0, 1]) = true

The recorded residue satisfies cop3Rp = cop3W + X.

theorem KoalaBear.sextic_cop3_bezout_check : CompPoly.RabinCert.eqModP fieldSize (CompPoly.RabinCert.addNat (CompPoly.RabinCert.mulNat SexticCert.cop3U sexticL) (CompPoly.RabinCert.mulNat SexticCert.cop3V SexticCert.cop3W)) [1] = true

The Bézout identity cop3U·f + cop3V·cop3W = 1 verifies.

Coprimality with X^(p^2) - X, the check for the prime factor 3 of 6

theorem KoalaBear.sextic_cop2_chain : CompPoly.RabinCert.runChain fieldSize sexticL [0, 1] SexticCert.cop2Steps = some SexticCert.cop2Rp

The 75-step chain for X^(p^2) mod f verifies and ends at the recorded residue.

theorem KoalaBear.sextic_cop2_exp : CompPoly.RabinCert.chainExp 1 SexticCert.cop2Steps = fieldSize ^ 2

The chain computes the exponent p^2.

theorem KoalaBear.sextic_cop2_w_check : CompPoly.RabinCert.eqModP fieldSize SexticCert.cop2Rp (CompPoly.RabinCert.addNat SexticCert.cop2W [0, 1]) = true

The recorded residue satisfies cop2Rp = cop2W + X.

theorem KoalaBear.sextic_cop2_bezout_check : CompPoly.RabinCert.eqModP fieldSize (CompPoly.RabinCert.addNat (CompPoly.RabinCert.mulNat SexticCert.cop2U sexticL) (CompPoly.RabinCert.mulNat SexticCert.cop2V SexticCert.cop2W)) [1] = true

The Bézout identity cop2U·f + cop2V·cop2W = 1 verifies.

theorem KoalaBear.sexticPoly_irreducible : Irreducible sexticPoly

X^6 + X^3 + 1 is irreducible over KoalaBear, by Rabin's test at a degree with two prime factors, with kernel-checked certificates for all three conditions.

instance KoalaBear.instFactIrreduciblePolynomialFieldSexticPoly : Fact (Irreducible sexticPoly)