21.3. HexGFqField: executable GF(pⁿ)🔗

21.3.1. Introduction🔗

HexGFqField constructs the field GF(pⁿ) = Fₚ[x] / (f) for a prime p and an irreducible degree-n modulus f of type Hex.FpPoly. It builds on the quotient ring documented in the HexGFqRing chapter: the field element type Hex.GFqField.FiniteField wraps a single Hex.GFqRing.PolyQuotient value, and every operation delegates to quotient-ring arithmetic and re-reduces, so the canonical-representative invariant from HexGFqRing carries over unchanged.

What the field adds over the ring is the structure that only exists when the modulus is irreducible: multiplicative inverses (via the polynomial extended GCD), division, integer powers, and the Frobenius endomorphism a ↦ aᵖ. Irreducibility is a hypothesis Hex.FpPoly.Irreducible carried in the type of every field element, discharged in practice by a checkable Rabin certificate from HexBerlekamp.

21.3.2. Field type and constructors🔗

A field element is a quotient-ring residue together with the modulus data and the irreducibility witness, all carried in the type. The hypotheses hf : 0 < FpPoly.degree f and hirr : FpPoly.Irreducible f (plus primality of p) appear as explicit arguments so that the field structure is only available where it is justified.

structure

Hex.GFqField.FiniteField {p : Nat} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) (hf : 0 < f.degree) (_hp : Hex.Nat.Prime p)
  (_hirr : f.Irreducible) : Type
Hex.GFqField.FiniteField {p : Nat}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree)
  (_hp : Hex.Nat.Prime p)
  (_hirr : f.Irreducible) : Type

Executable finite-field elements are a thin wrapper around quotient-ring residues modulo an irreducible polynomial.

Constructor

Hex.GFqField.FiniteField.mk

Fields

toQuotient : Hex.GFqRing.PolyQuotient f hf

The underlying reduced quotient-ring residue backing this field element.

Callers build elements through two smart constructors and read them back through one projection. Hex.GFqField.ofQuotient wraps an existing quotient residue, Hex.GFqField.ofPoly reduces a raw polynomial modulo the modulus, and Hex.GFqField.repr recovers the canonical representative, always of degree strictly below the modulus.

def

Hex.GFqField.ofQuotient {p : Nat} [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p} {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible} (x : Hex.GFqRing.PolyQuotient f hf) :
  Hex.GFqField.FiniteField f hf hp hirr
Hex.GFqField.ofQuotient {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  (x : Hex.GFqRing.PolyQuotient f hf) :
  Hex.GFqField.FiniteField f hf hp hirr

Wrap a quotient-ring element as a finite-field element.

def

Hex.GFqField.ofPoly {p : Nat} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree) (hp : Hex.Nat.Prime p) (hirr : f.Irreducible)
  (g : Hex.FpPoly p) : Hex.GFqField.FiniteField f hf hp hirr
Hex.GFqField.ofPoly {p : Nat}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree)
  (hp : Hex.Nat.Prime p)
  (hirr : f.Irreducible)
  (g : Hex.FpPoly p) :
  Hex.GFqField.FiniteField f hf hp hirr

Reduce a polynomial into the finite field by reusing the quotient-ring constructor.

def

Hex.GFqField.repr {p : Nat} [Hex.ZMod64.Bounds p] {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible}
  (x : Hex.GFqField.FiniteField f hf hp hirr) : Hex.FpPoly p
Hex.GFqField.repr {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  (x :
    Hex.GFqField.FiniteField f hf hp
      hirr) :
  Hex.FpPoly p

Project a finite-field element to its canonical polynomial representative.

The projection is canonical: representatives are always reduced below the modulus degree, and equality of field elements is equality of their quotient residues.

theorem

Hex.GFqField.degree_repr_lt_degree {p : Nat} [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p} {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible} (x : Hex.GFqField.FiniteField f hf hp hirr) :
  (Hex.GFqField.repr x).degree < f.degree
Hex.GFqField.degree_repr_lt_degree
  {p : Nat} [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  (x :
    Hex.GFqField.FiniteField f hf hp
      hirr) :
  (Hex.GFqField.repr x).degree < f.degree

Canonical field representatives are reduced below the modulus degree.

21.3.3. Field operations🔗

The ring operations delegate to the quotient ring: each wraps the corresponding Hex.GFqRing.PolyQuotient operation and rewraps the reduced result.

def

Hex.GFqField.add {p : Nat} [Hex.ZMod64.Bounds p] {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible}
  (x y : Hex.GFqField.FiniteField f hf hp hirr) :
  Hex.GFqField.FiniteField f hf hp hirr
Hex.GFqField.add {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  (x y :
    Hex.GFqField.FiniteField f hf hp
      hirr) :
  Hex.GFqField.FiniteField f hf hp hirr

Field addition reuses the quotient-ring sum.

def

Hex.GFqField.mul {p : Nat} [Hex.ZMod64.Bounds p] {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible}
  (x y : Hex.GFqField.FiniteField f hf hp hirr) :
  Hex.GFqField.FiniteField f hf hp hirr
Hex.GFqField.mul {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  (x y :
    Hex.GFqField.FiniteField f hf hp
      hirr) :
  Hex.GFqField.FiniteField f hf hp hirr

Field multiplication reuses the quotient-ring product.

def

Hex.GFqField.neg {p : Nat} [Hex.ZMod64.Bounds p] {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible}
  (x : Hex.GFqField.FiniteField f hf hp hirr) :
  Hex.GFqField.FiniteField f hf hp hirr
Hex.GFqField.neg {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  (x :
    Hex.GFqField.FiniteField f hf hp
      hirr) :
  Hex.GFqField.FiniteField f hf hp hirr

Field negation reuses the quotient-ring additive inverse.

def

Hex.GFqField.sub {p : Nat} [Hex.ZMod64.Bounds p] {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible}
  (x y : Hex.GFqField.FiniteField f hf hp hirr) :
  Hex.GFqField.FiniteField f hf hp hirr
Hex.GFqField.sub {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  (x y :
    Hex.GFqField.FiniteField f hf hp
      hirr) :
  Hex.GFqField.FiniteField f hf hp hirr

Field subtraction reuses the quotient-ring difference.

def

Hex.GFqField.pow {p : Nat} [Hex.ZMod64.Bounds p] {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible}
  (x : Hex.GFqField.FiniteField f hf hp hirr) (n : Nat) :
  Hex.GFqField.FiniteField f hf hp hirr
Hex.GFqField.pow {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  (x :
    Hex.GFqField.FiniteField f hf hp hirr)
  (n : Nat) :
  Hex.GFqField.FiniteField f hf hp hirr

Exponentiation reuses the quotient-ring repeated-multiplication path.

The constructors for literals reuse the quotient-ring casts, so natural and integer literals such as 0, 1, 7, and -3 denote field elements directly.

def

Hex.GFqField.natCast {p : Nat} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree) (hp : Hex.Nat.Prime p) (hirr : f.Irreducible)
  (n : Nat) : Hex.GFqField.FiniteField f hf hp hirr
Hex.GFqField.natCast {p : Nat}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree)
  (hp : Hex.Nat.Prime p)
  (hirr : f.Irreducible) (n : Nat) :
  Hex.GFqField.FiniteField f hf hp hirr

Natural-number literals reuse the quotient-ring cast and then rewrap the resulting reduced residue.

def

Hex.GFqField.intCast {p : Nat} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree) (hp : Hex.Nat.Prime p) (hirr : f.Irreducible)
  (i : Int) : Hex.GFqField.FiniteField f hf hp hirr
Hex.GFqField.intCast {p : Nat}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree)
  (hp : Hex.Nat.Prime p)
  (hirr : f.Irreducible) (i : Int) :
  Hex.GFqField.FiniteField f hf hp hirr

Integer literals reuse the quotient-ring cast and then rewrap the reduced residue.

The operations that need irreducibility come next. Inversion runs the polynomial extended GCD on the representative and the modulus, then normalizes the Bézout coefficient by the constant unit factor of the gcd. Irreducibility is exactly what forces that gcd to be a nonzero constant for any nonzero element. Division is multiplication by the inverse, and Frobenius is the p-th power map.

def

Hex.GFqField.inv {p : Nat} [Hex.ZMod64.Bounds p] {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible}
  (x : Hex.GFqField.FiniteField f hf hp hirr) :
  Hex.GFqField.FiniteField f hf hp hirr
Hex.GFqField.inv {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  (x :
    Hex.GFqField.FiniteField f hf hp
      hirr) :
  Hex.GFqField.FiniteField f hf hp hirr

Field inversion stays on the quotient-reduction path by reusing the polynomial extended-GCD witness, normalized by the gcd's constant unit factor. The 0 case follows the usual junk-value convention required by Lean.Grind.Field.

def

Hex.GFqField.div {p : Nat} [Hex.ZMod64.Bounds p] {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible}
  (x y : Hex.GFqField.FiniteField f hf hp hirr) :
  Hex.GFqField.FiniteField f hf hp hirr
Hex.GFqField.div {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  (x y :
    Hex.GFqField.FiniteField f hf hp
      hirr) :
  Hex.GFqField.FiniteField f hf hp hirr

Division is multiplication by the inverse candidate.

def

Hex.GFqField.frob {p : Nat} [Hex.ZMod64.Bounds p] {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible}
  (x : Hex.GFqField.FiniteField f hf hp hirr) :
  Hex.GFqField.FiniteField f hf hp hirr
Hex.GFqField.frob {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  (x :
    Hex.GFqField.FiniteField f hf hp
      hirr) :
  Hex.GFqField.FiniteField f hf hp hirr

The Frobenius map is the p-th power map on the existing quotient representation.

The standard typeclass instances Zero, One, Add, Mul, Neg, Sub, Pow, Inv, and Div on Hex.GFqField.FiniteField are backed by these operations, so ordinary field notation (x + y, x * y, -x, x - y, x ^ n, x⁻¹, and x / y) works over a Hex.GFqField.FiniteField.

21.3.3.1. Worked example: GF(5⁴) as F₅ modulo x⁴ + 2🔗

The example below builds the same modulus x⁴ + 2 used in the HexGFqRing worked example, whose reduction rule is x⁴ ≡ -2 ≡ 3 (mod 5), but now runs the field operations: inverses, division, and Frobenius alongside the ring operations. Irreducibility of the modulus is discharged by a Rabin Hex.Berlekamp.IrreducibilityCertificate, whose pow chain and Bézout witness are checked by the kernel-reducible Hex.Berlekamp.checkIrreducibilityCertificateLinear and routed to Hex.FpPoly.Irreducible through Hex.Berlekamp.rabinTest_imp_irreducible.

open Hex Hex.GFqField

namespace HexGFqFieldChapterExample

local instance boundsFive : ZMod64.Bounds 5 :=
  ⟨by⊢ 0 < 5 decideAll goals completed! 🐙, by⊢ 5 < 2 ^ 31 decideAll goals completed! 🐙⟩

private theorem prime_five : Hex.Nat.Prime 5 := by⊢ Nat.Prime 5
  constructorleft⊢ 2 ≤ 5right⊢ ∀ (m : Nat), m ∣ 5 → m = 1 ∨ m = 5
  ·left⊢ 2 ≤ 5 decideAll goals completed! 🐙
  ·right⊢ ∀ (m : Nat), m ∣ 5 → m = 1 ∨ m = 5 intro m hmrightm:Nathm:m ∣ 5⊢ m = 1 ∨ m = 5
    have hmle : m ≤ 5 :=
      Nat.le_of_dvd (bym:Nathm:m ∣ 5⊢ 0 < 5 decideAll goals completed! 🐙 : 0 < 5) hmrightm:Nathm:m ∣ 5hmle:m ≤ 5⊢ m = 1 ∨ m = 5
    have hcases :
        m = 0 ∨ m = 1 ∨ m = 2 ∨
        m = 3 ∨ m = 4 ∨ m = 5 := by⊢ Nat.Prime 5 omegarightm:Nathm:m ∣ 5hmle:m ≤ 5hcases:m = 0 ∨ m = 1 ∨ m = 2 ∨ m = 3 ∨ m = 4 ∨ m = 5⊢ m = 1 ∨ m = 5
    rcases hcases with
      rfl | rfl | rfl | rfl | rfl | rflright.inlhm:0 ∣ 5hmle:0 ≤ 5⊢ 0 = 1 ∨ 0 = 5right.inr.inlhm:1 ∣ 5hmle:1 ≤ 5⊢ 1 = 1 ∨ 1 = 5right.inr.inr.inlhm:2 ∣ 5hmle:2 ≤ 5⊢ 2 = 1 ∨ 2 = 5right.inr.inr.inr.inlhm:3 ∣ 5hmle:3 ≤ 5⊢ 3 = 1 ∨ 3 = 5right.inr.inr.inr.inr.inlhm:4 ∣ 5hmle:4 ≤ 5⊢ 4 = 1 ∨ 4 = 5right.inr.inr.inr.inr.inrhm:5 ∣ 5hmle:5 ≤ 5⊢ 5 = 1 ∨ 5 = 5
    ·right.inlhm:0 ∣ 5hmle:0 ≤ 5⊢ 0 = 1 ∨ 0 = 5 simp at hmAll goals completed! 🐙
    ·right.inr.inlhm:1 ∣ 5hmle:1 ≤ 5⊢ 1 = 1 ∨ 1 = 5 exact Or.inl rflAll goals completed! 🐙
    ·right.inr.inr.inlhm:2 ∣ 5hmle:2 ≤ 5⊢ 2 = 1 ∨ 2 = 5 simp at hmAll goals completed! 🐙
    ·right.inr.inr.inr.inlhm:3 ∣ 5hmle:3 ≤ 5⊢ 3 = 1 ∨ 3 = 5 simp at hmAll goals completed! 🐙
    ·right.inr.inr.inr.inr.inlhm:4 ∣ 5hmle:4 ≤ 5⊢ 4 = 1 ∨ 4 = 5 simp at hmAll goals completed! 🐙
    ·right.inr.inr.inr.inr.inrhm:5 ∣ 5hmle:5 ≤ 5⊢ 5 = 1 ∨ 5 = 5 exact Or.inr rflAll goals completed! 🐙

private instance : ZMod64.PrimeModulus 5 :=
  ZMod64.primeModulusOfPrime prime_five

/-- Monic degree-4 modulus x⁴ + 2 over F₅. -/
private def modulus : FpPoly 5 := #p[2, 0, 0, 0, 1]

private theorem modulus_pos_degree :
    0 < FpPoly.degree modulus := by⊢ 0 < modulus.degree decideAll goals completed! 🐙

private theorem modulus_monic :
    DensePoly.Monic modulus := by⊢ DensePoly.Monic modulus rflAll goals completed! 🐙

private theorem maxProperDiv_4 :
    Berlekamp.maximalProperDivisors 4 = [2] := by⊢ Berlekamp.maximalProperDivisors 4 = [2]
  decideAll goals completed! 🐙

/-- Rabin irreducibility certificate for x⁴ + 2. -/
private def cert :
    Berlekamp.IrreducibilityCertificate where
  p := 5
  n := 4
  powChain := #[
    #p[0, 1],
    #p[0, 3],
    #p[0, 4],
    #p[0, 2],
    #p[0, 1]
  ]
  bezout := #[
    { left := #p[3]
      right := #p[0, 0, 0, 4] }
  ]

set_option maxRecDepth 131072 in
set_option maxHeartbeats 8000000 in
private theorem cert_check :
    Berlekamp.checkIrreducibilityCertificateLinear
        modulus modulus_monic cert = true := by⊢ Berlekamp.checkIrreducibilityCertificateLinear modulus modulus_monic cert = true
  simp [Berlekamp.checkIrreducibilityCertificateLinear,
    cert, Berlekamp.IrreducibilityCertificate.toAmbient?,
    Berlekamp.checkPowChainLinear,
    Berlekamp.checkRabinBezoutWitnesses,
    Berlekamp.checkRabinBezoutWitness,
    Berlekamp.certifiedFrobeniusDiffMod,
    maxProperDiv_4, modulus]⊢ ((decide (4 = Berlekamp.basisSize (DensePoly.ofCoeffs #[2, 0, 0, 0, 1])) = true ∧
      ∀ (x : Nat),
        x < 5 →
          [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4],
                DensePoly.ofCoeffs #[0, 2], DensePoly.ofCoeffs #[0, 1]][x]? =
            some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ x)) ∧
    DensePoly.ofCoeffs #[0, 1] = FpPoly.modByMonic (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) FpPoly.X ⋯) ∧
  DensePoly.ofCoeffs #[3] * DensePoly.ofCoeffs #[2, 0, 0, 0, 1] +
      DensePoly.ofCoeffs #[0, 0, 0, 4] *
        (DensePoly.ofCoeffs #[0, 4] - FpPoly.modByMonic (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) FpPoly.X ⋯) =
    1
  constructorleft⊢ (decide (4 = Berlekamp.basisSize (DensePoly.ofCoeffs #[2, 0, 0, 0, 1])) = true ∧
    ∀ (x : Nat),
      x < 5 →
        [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
              DensePoly.ofCoeffs #[0, 1]][x]? =
          some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ x)) ∧
  DensePoly.ofCoeffs #[0, 1] = FpPoly.modByMonic (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) FpPoly.X ⋯right⊢ DensePoly.ofCoeffs #[3] * DensePoly.ofCoeffs #[2, 0, 0, 0, 1] +
    DensePoly.ofCoeffs #[0, 0, 0, 4] *
      (DensePoly.ofCoeffs #[0, 4] - FpPoly.modByMonic (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) FpPoly.X ⋯) =
  1
  ·left⊢ (decide (4 = Berlekamp.basisSize (DensePoly.ofCoeffs #[2, 0, 0, 0, 1])) = true ∧
    ∀ (x : Nat),
      x < 5 →
        [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
              DensePoly.ofCoeffs #[0, 1]][x]? =
          some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ x)) ∧
  DensePoly.ofCoeffs #[0, 1] = FpPoly.modByMonic (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) FpPoly.X ⋯ constructorleft.left⊢ decide (4 = Berlekamp.basisSize (DensePoly.ofCoeffs #[2, 0, 0, 0, 1])) = true ∧
  ∀ (x : Nat),
    x < 5 →
      [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
            DensePoly.ofCoeffs #[0, 1]][x]? =
        some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ x)left.right⊢ DensePoly.ofCoeffs #[0, 1] = FpPoly.modByMonic (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) FpPoly.X ⋯
    ·left.left⊢ decide (4 = Berlekamp.basisSize (DensePoly.ofCoeffs #[2, 0, 0, 0, 1])) = true ∧
  ∀ (x : Nat),
    x < 5 →
      [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
            DensePoly.ofCoeffs #[0, 1]][x]? =
        some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ x) constructorleft.left.left⊢ decide (4 = Berlekamp.basisSize (DensePoly.ofCoeffs #[2, 0, 0, 0, 1])) = trueleft.left.right⊢ ∀ (x : Nat),
  x < 5 →
    [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
          DensePoly.ofCoeffs #[0, 1]][x]? =
      some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ x)
      ·left.left.left⊢ decide (4 = Berlekamp.basisSize (DensePoly.ofCoeffs #[2, 0, 0, 0, 1])) = true rflAll goals completed! 🐙
      ·left.left.right⊢ ∀ (x : Nat),
  x < 5 →
    [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
          DensePoly.ofCoeffs #[0, 1]][x]? =
      some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ x) intro x hxleft.left.rightx:Nathx:x < 5⊢ [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
      DensePoly.ofCoeffs #[0, 1]][x]? =
  some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ x)
        have hcases :
            x = 0 ∨ x = 1 ∨ x = 2 ∨
            x = 3 ∨ x = 4 := by⊢ Berlekamp.checkIrreducibilityCertificateLinear modulus modulus_monic cert = true omegaleft.left.rightx:Nathx:x < 5hcases:x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4⊢ [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
      DensePoly.ofCoeffs #[0, 1]][x]? =
  some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ x)
        rcases hcases with
          rfl | rfl | rfl | rfl | rflleft.left.right.inlhx:0 < 5⊢ [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
      DensePoly.ofCoeffs #[0, 1]][0]? =
  some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ 0)left.left.right.inr.inlhx:1 < 5⊢ [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
      DensePoly.ofCoeffs #[0, 1]][1]? =
  some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ 1)left.left.right.inr.inr.inlhx:2 < 5⊢ [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
      DensePoly.ofCoeffs #[0, 1]][2]? =
  some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ 2)left.left.right.inr.inr.inr.inlhx:3 < 5⊢ [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
      DensePoly.ofCoeffs #[0, 1]][3]? =
  some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ 3)left.left.right.inr.inr.inr.inrhx:4 < 5⊢ [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
      DensePoly.ofCoeffs #[0, 1]][4]? =
  some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ 4) <;>left.left.right.inlhx:0 < 5⊢ [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
      DensePoly.ofCoeffs #[0, 1]][0]? =
  some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ 0)left.left.right.inr.inlhx:1 < 5⊢ [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
      DensePoly.ofCoeffs #[0, 1]][1]? =
  some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ 1)left.left.right.inr.inr.inlhx:2 < 5⊢ [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
      DensePoly.ofCoeffs #[0, 1]][2]? =
  some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ 2)left.left.right.inr.inr.inr.inlhx:3 < 5⊢ [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
      DensePoly.ofCoeffs #[0, 1]][3]? =
  some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ 3)left.left.right.inr.inr.inr.inrhx:4 < 5⊢ [DensePoly.ofCoeffs #[0, 1], DensePoly.ofCoeffs #[0, 3], DensePoly.ofCoeffs #[0, 4], DensePoly.ofCoeffs #[0, 2],
      DensePoly.ofCoeffs #[0, 1]][4]? =
  some (FpPoly.frobeniusXPowModLinear (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) ⋯ 4) rflAll goals completed! 🐙
    ·left.right⊢ DensePoly.ofCoeffs #[0, 1] = FpPoly.modByMonic (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) FpPoly.X ⋯ rflAll goals completed! 🐙
  ·right⊢ DensePoly.ofCoeffs #[3] * DensePoly.ofCoeffs #[2, 0, 0, 0, 1] +
    DensePoly.ofCoeffs #[0, 0, 0, 4] *
      (DensePoly.ofCoeffs #[0, 4] - FpPoly.modByMonic (DensePoly.ofCoeffs #[2, 0, 0, 0, 1]) FpPoly.X ⋯) =
  1 rflAll goals completed! 🐙

private theorem modulus_irreducible :
    FpPoly.Irreducible modulus :=
  have h :=
    Berlekamp.checkIrreducibilityCertificateLinear_rabinTest
      modulus modulus_monic cert cert_check
  Berlekamp.rabinTest_imp_irreducible
    modulus modulus_monic h

private abbrev F :=
  FiniteField modulus modulus_pos_degree
    prime_five modulus_irreducible

private def ff (f : FpPoly 5) : F :=
  ofPoly modulus modulus_pos_degree
    prime_five modulus_irreducible f

private def reprNats (x : F) : List Nat :=
  (repr x).toArray.toList.map ZMod64.toNat

private def a : F := ff #p[2, 3]
private def b : F := ff #p[4, 1, 0, 1]
private def x : F := ff #p[0, 1]

-- (2 + 3x) + (4 + x + x³) ≡ 1 + 4x + x³
#guard reprNats (a + b) = [1, 4, 0, 1]
-- (2 + 3x)(4 + x + x³), reduced via x⁴ ≡ 3
#guard reprNats (a * b) = [2, 4, 3, 2]
-- -(2 + 3x) ≡ 3 + 2x
#guard reprNats (-a) = [3, 2]
-- (2 + 3x) - (4 + x + x³) ≡ 3 + 2x + 4x³
#guard reprNats (a - b) = [3, 2, 0, 4]
-- x⁴ ≡ 3, the modulus relation
#guard reprNats (x ^ 4) = [3]
-- a⁻¹ from extended gcd: (2+3x)(1+x+x²+x³) ≡ 1
#guard reprNats a⁻¹ = [1, 1, 1, 1]
#guard a * a⁻¹ = 1
-- x⁻¹ = 2x³ since x·2x³ = 2x⁴ = 2·3 = 1
#guard reprNats x⁻¹ = [0, 0, 0, 2]
-- a / b = a · b⁻¹
#guard reprNats (a / b) = [2, 3, 3]
#guard a / b = a * b⁻¹
-- Frobenius x ↦ x⁵ : (2 + 3x)⁵ = 2 + 4x
#guard reprNats (frob a) = [2, 4]
#guard frob a = a ^ (5 : Nat)

end HexGFqFieldChapterExample

21.3.4. Key correctness theorems🔗

The proof obligations that promote the wrapper from a ring to a field are the inverse-cancellation laws. For any nonzero element, the extended-GCD inverse is a genuine two-sided multiplicative inverse.

theorem

Hex.GFqField.mul_inv_cancel {p : Nat} [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p} {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible} {x : Hex.GFqField.FiniteField f hf hp hirr}
  (hx : x ≠ 0) : x * x⁻¹ = 1
Hex.GFqField.mul_inv_cancel {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  {x :
    Hex.GFqField.FiniteField f hf hp hirr}
  (hx : x ≠ 0) : x * x⁻¹ = 1

A nonzero field element cancels against its inverse on the right.

theorem

Hex.GFqField.inv_mul_cancel {p : Nat} [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p} {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible} {x : Hex.GFqField.FiniteField f hf hp hirr}
  (hx : x ≠ 0) : x⁻¹ * x = 1
Hex.GFqField.inv_mul_cancel {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  {x :
    Hex.GFqField.FiniteField f hf hp hirr}
  (hx : x ≠ 0) : x⁻¹ * x = 1

A nonzero field element cancels against its inverse on the left.

Division is definitionally multiplication by the inverse, and the field is nontrivial (0 ≠ 1), which is where irreducibility (hence a positive-degree modulus) is used.

theorem

Hex.GFqField.div_eq_mul_inv {p : Nat} [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p} {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible} (x y : Hex.GFqField.FiniteField f hf hp hirr) :
  x / y = x * y⁻¹
Hex.GFqField.div_eq_mul_inv {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  (x y :
    Hex.GFqField.FiniteField f hf hp
      hirr) :
  x / y = x * y⁻¹

Division is field multiplication by inverse.

theorem

Hex.GFqField.zero_ne_one {p : Nat} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) (hf : 0 < f.degree) (hp : Hex.Nat.Prime p)
  (hirr : f.Irreducible) : 0 ≠ 1
Hex.GFqField.zero_ne_one {p : Nat}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree)
  (hp : Hex.Nat.Prime p)
  (hirr : f.Irreducible) : 0 ≠ 1

The quotient-field wrapper is nontrivial.

The Frobenius endomorphism is definitionally the p-th power map, the form downstream code uses.

theorem

Hex.GFqField.frob_eq_pow {p : Nat} [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p} {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible} (x : Hex.GFqField.FiniteField f hf hp hirr) :
  Hex.GFqField.frob x = x ^ p
Hex.GFqField.frob_eq_pow {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  (x :
    Hex.GFqField.FiniteField f hf hp
      hirr) :
  Hex.GFqField.frob x = x ^ p

Frobenius is definitionally the p-th power map.

These laws, together with the ring axioms inherited from HexGFqRing, are bundled into a Lean.Grind.Field instance on Hex.GFqField.FiniteField, plus a Lean.Grind.IsCharP instance recording characteristic p. That instance is the entry point for downstream proof automation over the executable finite field.

21.3.5. Cross-references🔗

HexGFqField has two upstream dependencies and serves the finite-field-valued callers downstream:

HexGFqRing (see its chapter) supplies the underlying Hex.GFqRing.PolyQuotient representation and all of the ring arithmetic. A Hex.GFqField.FiniteField is a one-field wrapper around a Hex.GFqRing.PolyQuotient, and every field operation reduces through the same Hex.GFqRing.reduceMod, so the canonical-representative invariant documented there carries over verbatim.
HexBerlekamp provides the irreducibility infrastructure. The Hex.FpPoly.Irreducible hypothesis carried by every field element is, in practice, produced from a checkable Rabin Hex.Berlekamp.IrreducibilityCertificate via Hex.Berlekamp.rabinTest_imp_irreducible, as shown in the worked example above.

Downstream, HexConway builds Conway polynomials and canonical GF(pⁿ) constructions on top of this field, reaching HexGFqRing transitively through HexGFqField.

21.3.5.1. No Mathlib correspondence library🔗

Like HexGFqRing, HexGFqField is a purely computational library with no paired *Mathlib correspondence: there is no HexGFqFieldMathlib, and this chapter therefore carries no "computational vs. Mathlib correspondence" cross-reference. The canonical mathematical home of GF(pⁿ) is Mathlib's GaloisField / AdjoinRoot construction. A correspondence between Hex.GFqField.FiniteField and those structures is deferred to a downstream library if and when a Mathlib-valued caller needs it.