15.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 FiniteField.

15.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

private instance : ZMod64.Bounds 5 :=
  ⟨by⊢ 0 < 5 decideAll goals completed! 🐙, by⊢ 5 ≤ UInt64.word decideAll goals completed! 🐙⟩

private theorem one_ne_zero_five :
    (1 : ZMod64 5) ≠ 0 := by⊢ 1 ≠ 0
  intro hh:1 = 0⊢ False
  have hm :=
    (ZMod64.natCast_eq_natCast_iff (p := 5) 1 0).mp hh:1 = 0hm:1 % 5 = 0 % 5⊢ False
  simp at hmAll 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

private def polyFive (coeffs : Array Nat) : FpPoly 5 :=
  FpPoly.ofCoeffs
    (coeffs.map (fun n => ZMod64.ofNat 5 n))

/-- Monic degree-4 modulus x⁴ + 2 over F₅. -/
private def modulus : FpPoly 5 :=
  { coeffs := #[(2 : ZMod64 5), 0, 0, 0, 1]
    normalized := by⊢ DensePolyNormalized #[2, 0, 0, 0, 1]
      right⊢ #[2, 0, 0, 0, 1].back? ≠ some Zero.zero
      decideAll goals completed! 🐙 }

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 :=
    #[polyFive #[0, 1], polyFive #[0, 3],
      polyFive #[0, 4], polyFive #[0, 2],
      polyFive #[0, 1]]
  bezout :=
    #[{ left := polyFive #[3]
        right := polyFive #[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, polyFive]⊢ ((4 = Berlekamp.basisSize { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ∧
      ∀ (x : Nat),
        x < 5 →
          [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
                FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4],
                FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
                FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][x]? =
            some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ x)) ∧
    FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1] =
      FpPoly.modByMonic { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } FpPoly.X ⋯) ∧
  FpPoly.ofCoeffs #[ZMod64.ofNat 5 3] * { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } +
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 0, ZMod64.ofNat 5 0, ZMod64.ofNat 5 4] *
        (FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4] -
          FpPoly.modByMonic { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } FpPoly.X ⋯) =
    1
  constructorleft⊢ (4 = Berlekamp.basisSize { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ∧
    ∀ (x : Nat),
      x < 5 →
        [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
              FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4],
              FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
              FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][x]? =
          some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ x)) ∧
  FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1] =
    FpPoly.modByMonic { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } FpPoly.X ⋯right⊢ FpPoly.ofCoeffs #[ZMod64.ofNat 5 3] * { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } +
    FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 0, ZMod64.ofNat 5 0, ZMod64.ofNat 5 4] *
      (FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4] -
        FpPoly.modByMonic { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } FpPoly.X ⋯) =
  1
  ·left⊢ (4 = Berlekamp.basisSize { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ∧
    ∀ (x : Nat),
      x < 5 →
        [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
              FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4],
              FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
              FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][x]? =
          some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ x)) ∧
  FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1] =
    FpPoly.modByMonic { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } FpPoly.X ⋯ constructorleft.left⊢ 4 = Berlekamp.basisSize { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ∧
  ∀ (x : Nat),
    x < 5 →
      [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
            FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4],
            FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
            FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][x]? =
        some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ x)left.right⊢ FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1] =
  FpPoly.modByMonic { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } FpPoly.X ⋯
    ·left.left⊢ 4 = Berlekamp.basisSize { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ∧
  ∀ (x : Nat),
    x < 5 →
      [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
            FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4],
            FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
            FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][x]? =
        some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ x) constructorleft.left.left⊢ 4 = Berlekamp.basisSize { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 }left.left.right⊢ ∀ (x : Nat),
  x < 5 →
    [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
          FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
          FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][x]? =
      some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ x)
      ·left.left.left⊢ 4 = Berlekamp.basisSize { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } rflAll goals completed! 🐙
      ·left.left.right⊢ ∀ (x : Nat),
  x < 5 →
    [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
          FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
          FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][x]? =
      some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ x) intro x hxleft.left.rightx:Nathx:x < 5⊢ [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][x]? =
  some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_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⊢ [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][x]? =
  some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ x)
        rcases hcases with
          rfl | rfl | rfl | rfl | rflleft.left.right.inlhx:0 < 5⊢ [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][0]? =
  some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ 0)left.left.right.inr.inlhx:1 < 5⊢ [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][1]? =
  some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ 1)left.left.right.inr.inr.inlhx:2 < 5⊢ [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][2]? =
  some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ 2)left.left.right.inr.inr.inr.inlhx:3 < 5⊢ [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][3]? =
  some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ 3)left.left.right.inr.inr.inr.inrhx:4 < 5⊢ [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][4]? =
  some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ 4) <;>left.left.right.inlhx:0 < 5⊢ [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][0]? =
  some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ 0)left.left.right.inr.inlhx:1 < 5⊢ [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][1]? =
  some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ 1)left.left.right.inr.inr.inlhx:2 < 5⊢ [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][2]? =
  some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ 2)left.left.right.inr.inr.inr.inlhx:3 < 5⊢ [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][3]? =
  some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ 3)left.left.right.inr.inr.inr.inrhx:4 < 5⊢ [FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 3],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4], FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 2],
      FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1]][4]? =
  some (FpPoly.frobeniusXPowModLinear { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } ⋯ 4) rflAll goals completed! 🐙
    ·left.right⊢ FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 1] =
  FpPoly.modByMonic { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } FpPoly.X ⋯ rflAll goals completed! 🐙
  ·right⊢ FpPoly.ofCoeffs #[ZMod64.ofNat 5 3] * { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_1 } +
    FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 0, ZMod64.ofNat 5 0, ZMod64.ofNat 5 4] *
      (FpPoly.ofCoeffs #[ZMod64.ofNat 5 0, ZMod64.ofNat 5 4] -
        FpPoly.modByMonic { coeffs := #[2, 0, 0, 0, 1], normalized := modulus._proof_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 (coeffs : Array Nat) : F :=
  ofPoly modulus modulus_pos_degree
    prime_five modulus_irreducible (polyFive coeffs)

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

private def a : F := ff #[2, 3]
private def b : F := ff #[4, 1, 0, 1]
private def x : F := ff #[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