hex

21.5. HexGFq: canonical finite-field constructors🔗

21.5.1. Introduction🔗

HexGFq packages the committed Conway-table entries of HexConway as ready-to-use field types, so a caller who wants GF(pⁿ) for a supported pair (p, n) never has to supply a modulus or an irreducibility proof by hand. It builds on the executable field HexGFqField, the Conway lookup HexConway, and the packed characteristic-two field HexGF2.

It exposes two parallel families of constructors. The generic family builds every field as the HexGFqField quotient `Fₚ[x] / (f)` with f the committed Conway modulus, and works for every committed (p, n). The packed characteristic-two family, for committed binary entries, instead routes through the single-word HexGF2 representation, trading the generic quotient for machine-word arithmetic while certifying, at elaboration time, that the packed modulus is the same Conway polynomial. HexGFq is Mathlib-free. Everything below typechecks against the executable libraries only.

21.5.2. The committed-entry mechanism🔗

The generic constructors need a Hex.Conway.SupportedEntry, the HexConway witness bundling a Conway modulus with its primality and irreducibility proofs. Passing that witness explicitly everywhere is verbose, so HexGFq makes it available through instance synthesis with a one-method class.

Hex.Conway.CommittedEntry carries a single field entry, the committed Hex.Conway.SupportedEntry for the pair (p, n). The library commits one instance per committed table cell, named committedEntry_p_n (for example committedEntry_2_3), covering p ∈ {2, 3, 5, 7, 11, 13}, to n = 6 for the odd primes and to n = 8 for p = 2. With the instance in scope, the short field spelling resolves the witness automatically. Where a proof needs to name the witness, the explicit form still takes it as an argument.

21.5.3. Generic constructors🔗

The headline type is Hex.GFq: given an explicit Hex.Conway.SupportedEntry for (p, n), it is the HexGFqField finite field over the committed Conway modulus, with the positive-degree, primality, and irreducibility hypotheses discharged from the entry. Its ergonomic sibling Hex.GFqC is the same field with the entry resolved by Hex.Conway.CommittedEntry synthesis, so GFqC 2 3 denotes GF(8) with no further arguments.

Each field element is a polynomial over F_p of degree below n: the remainder of an Hex.FpPoly modulo the field's Conway polynomial. repr returns that remainder. The generic constructor reduces an arbitrary Hex.FpPoly to it:

🔗def
Hex.GFq.ofPoly {p n : ℕ} [Hex.ZMod64.Bounds p]
  (h : Hex.Conway.SupportedEntry p n) (g : Hex.FpPoly p) : Hex.GFq p n h
Hex.GFq.ofPoly {p n : ℕ}
  [Hex.ZMod64.Bounds p]
  (h : Hex.Conway.SupportedEntry p n)
  (g : Hex.FpPoly p) : Hex.GFq p n h

Reduce a polynomial into the canonical field selected by a committed Conway entry.

The committed-entry constructor delegates to it, resolving the witness from the ambient instance:

🔗def
Hex.GFqC.ofPoly {p n : ℕ} [Hex.ZMod64.Bounds p]
  [h : Hex.Conway.CommittedEntry p n] (g : Hex.FpPoly p) : Hex.GFqC p n
Hex.GFqC.ofPoly {p n : ℕ}
  [Hex.ZMod64.Bounds p]
  [h : Hex.Conway.CommittedEntry p n]
  (g : Hex.FpPoly p) : Hex.GFqC p n

Reduce a polynomial into the committed GFqC p n field.

A family of *_eq_gfq lemmas characterises the Hex.GFqC spelling against the explicit Hex.GFq one, so a proof may always unfold the convenience spelling back to the entry-explicit form. The modulus delegation is representative:

🔗theorem
Hex.GFqC.modulus_eq_gfq {p n : ℕ} [Hex.ZMod64.Bounds p]
  [h : Hex.Conway.CommittedEntry p n] :
  Hex.GFqC.modulus = Hex.GFq.modulus Hex.GFqC.entry
Hex.GFqC.modulus_eq_gfq {p n : ℕ}
  [Hex.ZMod64.Bounds p]
  [h : Hex.Conway.CommittedEntry p n] :
  Hex.GFqC.modulus =
    Hex.GFq.modulus Hex.GFqC.entry

Hex.GFqC.modulus delegates to the explicit-entry Hex.GFq.modulus.

Both families provide the full executable field API: repr, the ring and field operations, and the Frobenius endomorphism a ↦ aᵖ as the p-th power map.

🔗def
Hex.GFq.frob {p n : ℕ} [Hex.ZMod64.Bounds p]
  {h : Hex.Conway.SupportedEntry p n} (x : Hex.GFq p n h) :
  Hex.GFq p n h
Hex.GFq.frob {p n : ℕ}
  [Hex.ZMod64.Bounds p]
  {h : Hex.Conway.SupportedEntry p n}
  (x : Hex.GFq p n h) : Hex.GFq p n h

The Frobenius endomorphism on the canonical Conway-backed field, computed as the p-th power on the underlying quotient representation.

21.5.4. Packed characteristic-two constructors🔗

For committed binary entries (2, n), the generic quotient is heavier than necessary: the field has a single-word packed representation in HexGF2. HexGFq exposes that fast path alongside the generic one and proves the two agree.

The translation from a packed single-word modulus to the generic FpPoly 2 view is:

🔗def
Hex.Conway.packedGF2FpPoly (lower : UInt64) (n : ℕ) : Hex.FpPoly 2
Hex.Conway.packedGF2FpPoly
  (lower : UInt64) (n : ℕ) : Hex.FpPoly 2

Interpret a packed single-word binary modulus as the corresponding generic FpPoly 2 polynomial. lower supplies the coefficients of degrees < n; the leading degree-n coefficient is inserted explicitly.

A committed binary entry that also admits the packed view is recorded by the class Hex.Conway.PackedGF2Entry. Its fields bundle the HexConway Hex.Conway.SupportedEntry, the packed lower-word modulus Hex.Conway.PackedGF2Entry.lower, the extension-degree bounds 0 < n < 64, the certified irreducibility of the packed modulus, and (crucially) Hex.Conway.PackedGF2Entry.conway_eq_packed, the proof that the committed Conway polynomial equals the packed modulus viewed as an Hex.FpPoly with modulus 2. That equality is what lets the optimized field stand in for the canonical one without changing the mathematics. The committed instances are named packedGF2Entry_2_n.

The optimized field itself is Hex.GF2q: for a committed Hex.Conway.PackedGF2Entry at degree n, the single-word HexGF2 field Hex.GF2n with that modulus. A UInt64 word becomes a packed element through:

🔗def
Hex.GF2q.ofWord {n : ℕ} [h : Hex.Conway.PackedGF2Entry n] (w : UInt64) :
  Hex.GF2q n
Hex.GF2q.ofWord {n : ℕ}
  [h : Hex.Conway.PackedGF2Entry n]
  (w : UInt64) : Hex.GF2q n

Reduce a machine word into the optimized binary field selected by a committed packed Conway entry.

and the map from a packed element to its generic Hex.GFq counterpart is:

🔗def
Hex.GF2q.toGFq {n : ℕ} [h : Hex.Conway.PackedGF2Entry n]
  (x : Hex.GF2q n) : Hex.GFq 2 n Hex.GF2q.supportedEntry
Hex.GF2q.toGFq {n : ℕ}
  [h : Hex.Conway.PackedGF2Entry n]
  (x : Hex.GF2q n) :
  Hex.GFq 2 n Hex.GF2q.supportedEntry

Map an optimized packed canonical binary-field element into the generic canonical GFq 2 n model for the same committed Conway entry.

21.5.5. Worked example🔗

The committed pair (2, 3) gives GF(8) = 𝔽₂[x] / (x³ + x + 1), the Conway field C(2, 3). The block below spells GF(8) two ways (the generic GFqC 2 3 and the packed GF2q 3), then computes with the packed representation, where elements are machine words whose bits are the polynomial coefficients (bit i is the coefficient of xⁱ).

open Hex namespace HexGFqChapter -- Both spellings of GF(8) resolve via instance -- synthesis on the committed (2, 3) entry. GFqC 2 3 : Type#check (GFqC 2 3) GF2q 3 : Type#check (GF2q 3) -- Packed elements of GF(8); bit i is the xⁱ coeff. abbrev E := GF2q 3 def ofW (w : UInt64) : E := GF2q.ofWord w -- x = 0b010, x² = 0b100. -- x · x² = x³ ≡ x + 1 = 0b011, since x³+x+1 = 0. #guard GF2q.repr (ofW 2 * ofW 4) = 3 -- x · x = x² = 0b100. #guard GF2q.repr (ofW 2 * ofW 2) = 4 -- x⁴ = x·x³ ≡ x²+x = 0b110. #guard GF2q.repr (ofW 4 * ofW 4) = 6 -- Addition is XOR: (x+1) + (x²+1) = x²+x = 0b110. #guard GF2q.repr (ofW 3 + ofW 5) = 6 -- x⁻¹ = x²+1 = 0b101, since x·(x²+1) = x³+x = 1. #guard GF2q.repr (ofW 2)⁻¹ = 5 #guard GF2q.repr (ofW 2 * (ofW 2)⁻¹) = 1 end HexGFqChapter

21.5.6. Key correctness: Lean-checked irreducibility🔗

A finite field exists only when its modulus is irreducible, so every constructor in this library ultimately rests on an irreducibility proof. For the generic constructors that proof is the HexConway entry's; for the packed constructors it is a separate certificate over the HexGF2 Hex.GF2Poly.Irreducible predicate, discharged by decide on a checkable certificate, never by native_decide. The degree-one case is small enough to prove by exhausting the two monic linear polynomials over 𝔽₂:

🔗theorem
Hex.Conway.packedGF2Entry_2_1_irreducible :
  (Hex.GF2Poly.ofUInt64Monic 1 1).Irreducible
Hex.Conway.packedGF2Entry_2_1_irreducible :
  (Hex.GF2Poly.ofUInt64Monic 1
      1).Irreducible

The packed modulus corresponding to the committed Conway entry C(2, 1) = X + 1.

Higher-degree committed entries are certified the same way through the HexGF2 certificate checker. Because the check runs at elaboration time, a corrupted packed modulus would fail to typecheck rather than silently producing a non-field, so the irreducible-modulus guarantee is checked when the library compiles, not a runtime assertion.

21.5.7. The Mathlib correspondence🔗

Everything above is executable and Mathlib-free. HexGFqMathlib connects it to Mathlib: for prime p, the executable field Hex.GFq is ring-isomorphic to Mathlib's GaloisField p n, with p ^ n elements.

🔗def
HexGFqMathlib.GFq.equivGaloisField {p n : ℕ} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p] [Fact (Nat.Prime p)]
  (h : Hex.Conway.SupportedEntry p n) (hn : n ≠ 0) :
  Hex.GFq p n h ≃+* GaloisField p n
HexGFqMathlib.GFq.equivGaloisField
  {p n : ℕ} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  [Fact (Nat.Prime p)]
  (h : Hex.Conway.SupportedEntry p n)
  (hn : n ≠ 0) :
  Hex.GFq p n h ≃+* GaloisField p n

Canonical Hex.GFq values are ring-equivalent to Mathlib's GaloisField with the same characteristic and extension degree.

🔗theorem
HexGFqMathlib.GFq.fintype_card_eq_pow {p n : ℕ} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p] (h : Hex.Conway.SupportedEntry p n) :
  Fintype.card (Hex.GFq p n h) = p ^ n
HexGFqMathlib.GFq.fintype_card_eq_pow
  {p n : ℕ} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  (h : Hex.Conway.SupportedEntry p n) :
  Fintype.card (Hex.GFq p n h) = p ^ n

Cardinality of canonical GFq p n as p ^ n.

🔗theorem
HexGFqMathlib.GFq.card_eq_galoisField_card {p n : ℕ}
  [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] [Fact (Nat.Prime p)]
  (h : Hex.Conway.SupportedEntry p n) (hn : n ≠ 0) :
  Fintype.card (Hex.GFq p n h) = Nat.card (GaloisField p n)
HexGFqMathlib.GFq.card_eq_galoisField_card
  {p n : ℕ} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  [Fact (Nat.Prime p)]
  (h : Hex.Conway.SupportedEntry p n)
  (hn : n ≠ 0) :
  Fintype.card (Hex.GFq p n h) =
    Nat.card (GaloisField p n)

Canonical Hex.GFq and Mathlib's GaloisField have matching cardinalities.

21.5.8. Cross-references🔗

HexGFq is the aggregator of the finite-field constructor libraries:

  • HexConway supplies the committed Conway moduli and their Hex.Conway.SupportedEntry witnesses; each Hex.Conway.CommittedEntry instance wraps one.

  • HexGFqField (over HexGFqRing) is the generic quotient field backing Hex.GFq and Hex.GFqC; every generic operation delegates to it.

  • HexGF2 provides the single-word packed field Hex.GF2n backing Hex.GF2q, together with the Hex.GF2Poly.Irreducible predicate the packed certificates discharge.

HexGFq is Mathlib-free. Its Mathlib correspondence (above, via HexGFqMathlib) identifies the executable field with Mathlib's GaloisField.