The degree-6 extension of KoalaBear

KoalaBear[X] / (X^6 + X^3 + 1), a field of p^6 ≈ 2^186 elements. The modulus is Φ₉, the ninth cyclotomic polynomial, so the adjoined root θ is a primitive 9th root of unity.

As at degree 5, the modulus is necessarily not a binomial, and for a stronger reason: since p - 1 = 2^24 · 127 we have 3 ∤ p - 1, so 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. So no degree-6 binomial extension of KoalaBear exists at all.

Φ₉ is chosen among the irreducible sextics because every entry of its reduction table X^6 … X^10 mod f is ±1 — reduction costs no base-field multiplications — and the same holds for its Frobenius matrix, since p ≡ 2 mod 9 makes Frobenius θ ↦ θ^2. It also carries the 2-then-3 tower implicitly: θ^3 is a primitive cube root of unity generating the F_p² subfield, because Y^2 + Y + 1 is irreducible over KoalaBear.

Irreducibility of X^6 + X^3 + 1 is KoalaBear.sexticPoly_irreducible (CompPoly/Fields/KoalaBear/Ext6/SexticIrreducible.lean), proved by Rabin's test at a degree with two prime factors, with kernel-checked certificates for all three conditions. Supporting files live under KoalaBear/Ext6/.

This sits alongside KoalaBear.Ext5 rather than replacing it; the two are independent instances of the same framework.

Main definitions

• KoalaBear.ext6Params: the ExtensionParams for X^6 + X^3 + 1.
• KoalaBear.Ext6: the extension field itself.

def KoalaBear.ext6Params : CompPoly.Extension.ExtensionParams Field

The parameters of the sextic extension KoalaBear[X] / (X^6 + X^3 + 1): the lower coefficients of the monic modulus are (1, 0, 0, 1, 0, 0).

instance KoalaBear.instFactEqNatCardFieldQExt6Params : Fact (Nat.card Field = ext6Params.q)

@[simp]

theorem KoalaBear.ext6Params_d : ext6Params.d = 6

@[simp]

theorem KoalaBear.ext6Params_q : ext6Params.q = fieldSize

theorem KoalaBear.ext6Params_poly : ext6Params.poly = sexticPoly

The defining polynomial of the parameters is the sextic X^6 + X^3 + 1.

instance KoalaBear.instFactIrreduciblePolynomialFieldPolyExt6Params : Fact (Irreducible ext6Params.poly)

The irreducibility fact in the form the framework's Field instance consumes.

@[reducible, inline]

abbrev KoalaBear.Ext6 : Type

The degree-6 extension field of KoalaBear.

def KoalaBear.ext6Gen : Ext6

The adjoined root of X^6 + X^3 + 1, a primitive 9th root of unity, as an element of Ext6.

theorem KoalaBear.ext6Gen_eq_gen : ext6Gen = CompPoly.Extension.Ext.gen

ext6Gen is the framework's Ext.gen.

Deliberately not @[simp]: as a rewrite it fires before ext6Gen_pow_six can match, which would knock that lemma out of the simp set.

@[simp]

theorem KoalaBear.toQuot_ext6Gen : CompPoly.Extension.Ext.toQuot ext6Gen = CompPoly.Extension.Ext.rt ext6Params

ext6Gen maps to the adjoined root of the specification.

theorem KoalaBear.aeval_ext6Gen : (Polynomial.aeval ext6Gen) ext6Params.poly = 0

ext6Gen is a root of X^6 + X^3 + 1, in the form aeval expects.

@[simp]

theorem KoalaBear.ext6Gen_pow_six : ext6Gen ^ 6 = -ext6Gen ^ 3 - CompPoly.Extension.Ext.ofBase 1

The defining relation: the adjoined root satisfies θ^6 = -θ^3 - 1. Every coefficient is ±1, which is what makes reduction multiplication-free.

theorem KoalaBear.ext6Gen_cubed_is_primitive_cube_root : (ext6Gen ^ 3) ^ 2 + ext6Gen ^ 3 + CompPoly.Extension.Ext.ofBase 1 = 0

θ^3 is a primitive cube root of unity: it satisfies Y^2 + Y + 1 = 0, which is irreducible over KoalaBear because 3 ∤ p - 1. So F_p(θ^3) is the F_p² subfield, and this is the 2-then-3 tower F_p ⊂ F_p² ⊂ F_p⁶ presented inside a single sextic.

@[simp]

theorem KoalaBear.ext6Gen_pow_nine : ext6Gen ^ 9 = 1

θ is a primitive 9th root of unity: θ^9 = 1.

@[simp]

theorem KoalaBear.card_ext6 : Fintype.card Ext6 = fieldSize ^ 6