hex

19.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]
  [Hex.ZMod64.PrimeModulus 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]
  [Hex.ZMod64.PrimeModulus 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]
  [Hex.ZMod64.PrimeModulus 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]
  [Hex.ZMod64.PrimeModulus 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.

19.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. All of that is committed once as Hex.GFqField.Example.modulus, so the example below cites the result rather than rebuilding a certificate inline.

🔗def
Hex.GFqField.Example.modulus : Hex.FpPoly 5
Hex.GFqField.Example.modulus :
  Hex.FpPoly 5

A monic degree-four modulus x⁴ + 2 over 𝔽₅, committed with its irreducibility certificate so that a small GF(5⁴) is available without hand-writing one. Used by the manual's worked examples and by conformance.

🔗theorem
Hex.GFqField.Example.modulus_irreducible :
  Hex.GFqField.Example.modulus.Irreducible
Hex.GFqField.Example.modulus_irreducible :
  Hex.GFqField.Example.modulus.Irreducible

The example modulus is irreducible, by routing the checked certificate through Rabin soundness.

🔗def
Hex.GFqField.Example.F : Type
Hex.GFqField.Example.F : Type

The example field GF(5⁴).

open Hex Hex.GFqField namespace HexGFqFieldChapterExample open GFqField.Example (boundsFive prime_five) private abbrev F := GFqField.Example.F private def ff (f : FpPoly 5) : F := GFqField.Example.ofPoly 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