21.4. HexConway: Tier 1 Conway-polynomial lookup🔗

21.4.1. Introduction🔗

A Conway polynomial C(p, n) is the canonical irreducible degree-n polynomial over the prime field 𝔽_p used to give a standard, compatible presentation of the finite field 𝔽_{pⁿ}. The full treatment of Conway polynomials has three tiers: a Tier 1 lookup of committed table entries, Tier 2 proofs that those entries satisfy the Conway compatibility conditions across the subfield lattice, and Tier 3 search for entries beyond the committed table. HexConway currently implements Tier 1 only: it exposes the imported Lübeck Conway table as a lookup, keeping the baseline lookup separate from the later compatibility and search work.

HexConway is Mathlib-free. It depends only on HexBerlekamp (for the Rabin irreducibility checker that certifies each committed entry) and the prime-field polynomial library it reaches through it. Each supported (p, n) pair commits a named polynomial literal, a machine-checked irreducibility proof, and a Hex.Conway.SupportedEntry witness packaging the lookup together with its proof. See Cross-references.

21.4.2. The lookup🔗

The committed data is a raw coefficient table, stored ascending by degree and keyed on the pair (p, n). It returns none on any pair outside the committed table.

def

Hex.Conway.luebeckConwayCoeffs? : Nat → Nat → Option (List Nat)
Hex.Conway.luebeckConwayCoeffs? :
  Nat → Nat → Option (List Nat)

Committed Lübeck Conway-table coefficients, stored ascending by degree.

A small builder turns a list of natural-number coefficients into an FpPoly p by reducing each coefficient into ZMod64 p and routing through the normalizing constructor.

def

Hex.Conway.luebeckConwayPolynomialOfCoeffs (p : Nat)
  [Hex.ZMod64.Bounds p] (coeffs : List Nat) : Hex.FpPoly p
Hex.Conway.luebeckConwayPolynomialOfCoeffs
  (p : Nat) [Hex.ZMod64.Bounds p]
  (coeffs : List Nat) : Hex.FpPoly p

Build an FpPoly p from ascending natural-number coefficients.

The main entry point composes the two: it looks up the coefficient list and, on a hit, builds the polynomial. The supported coverage is p ∈ {2, 3, 5, 7, 11, 13}, running to n = 6 for the odd primes and to n = 8 for p = 2, so GF(2⁸) is a committed Conway field. Every other pair returns none rather than triggering Tier 2 compatibility checks or Tier 3 search.

The binary column runs further because cost decides the scope: the committed entries carry Rabin certificates that the kernel replays, and that replay is cheapest over 𝔽₂, where every residue is one bit. The scope is therefore a maximum degree per prime rather than one bound for all of them, and widening it is a matter of measuring rather than of finding new mathematics.

def

Hex.Conway.luebeckConwayPolynomial? (p n : Nat) [Hex.ZMod64.Bounds p] :
  Option (Hex.FpPoly p)
Hex.Conway.luebeckConwayPolynomial?
  (p n : Nat) [Hex.ZMod64.Bounds p] :
  Option (Hex.FpPoly p)

Tier 1 imported-table lookup for committed Luebeck Conway entries.

This is only the imported-table surface: unsupported pairs return none rather than triggering Tier 2 compatibility checks or Tier 3 search.

21.4.3. The supported-entry witness🔗

For each supported pair the library commits a Hex.Conway.SupportedEntry, a record bundling the looked-up polynomial with the two facts that make it a genuine Conway modulus: a primality witness prime : Hex.Nat.Prime p for the field characteristic, and a proof isSupported that Hex.Conway.luebeckConwayPolynomial? actually resolves to the stored polynomial at (p, n). The accessor reads the modulus back out.

Hex.Conway.SupportedEntry therefore certifies that a lookup is a hit, not just that a polynomial exists. The committed witnesses are named supportedEntry_p_n (for example Hex.Conway.supportedEntry_2_3).

def

Hex.Conway.conwayPoly (p n : Nat) [Hex.ZMod64.Bounds p]
  (h : Hex.Conway.SupportedEntry p n) : Hex.FpPoly p
Hex.Conway.conwayPoly (p n : Nat)
  [Hex.ZMod64.Bounds p]
  (h : Hex.Conway.SupportedEntry p n) :
  Hex.FpPoly p

Recover the committed Conway modulus for a supported entry.

21.4.4. Worked example🔗

The block below runs the lookup on the supported pair (2, 3) (the Conway polynomial C(2, 3) = 1 + x + x³ over 𝔽₂) and on two unsupported pairs.

open Hex Hex.Conway

namespace HexConwayChapter

-- The committed table stores C(2,3) ascending by
-- degree: 1 + x + x³.
#guard luebeckConwayCoeffs? 2 3 = some [1, 1, 0, 1]

-- The lookup builds the FpPoly from those
-- coefficients, hitting the committed literal.
#guard luebeckConwayPolynomial? 2 3 =
  some luebeckConwayPolynomial_2_3

-- The SupportedEntry witness packages the same hit,
-- and conwayPoly reads the modulus back out.
#guard supportedEntry_2_3.poly =
  luebeckConwayPolynomial_2_3
#guard conwayPoly 2 3 supportedEntry_2_3 =
  luebeckConwayPolynomial_2_3

-- Unsupported pairs return none rather than
-- searching. The binary column runs to degree 8,
-- the odd primes to 6.
#guard luebeckConwayPolynomial? 2 8 =
  some luebeckConwayPolynomial_2_8
#guard luebeckConwayPolynomial? 2 9 =
  (none : Option (FpPoly 2))
#guard luebeckConwayPolynomial? 3 7 =
  (none : Option (FpPoly 3))
#guard luebeckConwayPolynomial? 2 0 =
  (none : Option (FpPoly 2))

end HexConwayChapter

21.4.5. Key correctness theorem🔗

The point of committing a table rather than computing on demand is that each entry carries a machine-checked irreducibility proof. For every supported pair the library proves luebeckConwayPolynomial_p_n_irreducible : FpPoly.Irreducible luebeckConwayPolynomial_p_n, discharged by running the Berlekamp Rabin irreducibility certificate checker, whose soundness is Hex.Berlekamp.rabinTest_imp_irreducible, on a committed certificate. The representative statement for C(2, 3):

theorem

Hex.Conway.luebeckConwayPolynomial_2_3_irreducible :
  Hex.Conway.luebeckConwayPolynomial_2_3.Irreducible
Hex.Conway.luebeckConwayPolynomial_2_3_irreducible :
  Hex.Conway.luebeckConwayPolynomial_2_3.Irreducible

The committed C(2, 3) entry is irreducible.

Because the certificate is checked at elaboration time, the irreducible factor structure of the committed table is part of the library's guarantee, not a runtime assertion: a corrupted entry would fail to typecheck rather than silently return a reducible polynomial.

21.4.6. Cross-references🔗

HexConway is near the top of the finite-field portion of the DAG:

HexBerlekamp is the direct dependency. Its Rabin irreducibility test and the soundness theorem Hex.Berlekamp.rabinTest_imp_irreducible (lifting a passing certificate to Hex.FpPoly.Irreducible) certify every committed entry in the correctness section. The prime-field polynomial type Hex.FpPoly and its arithmetic are reached transitively through it.
Tier 2 and Tier 3 belong to this library and are not yet implemented. Until Tier 2 lands, what Lean checks about a committed entry is that it is monic, irreducible, and of the requested degree. That it is the Conway polynomial for its pair, rather than some other irreducible of the same degree, rests on the imported Lübeck table and is checked outside Lean by the conformance oracle. Nothing downstream is weakened by this: GFq p n is a genuine field of order pⁿ either way. What is not yet available is the compatibility across the subfield lattice that motivates the Conway choice in the first place.
HexConway is Mathlib-free and never depends on Mathlib. The Mathlib correspondence proofs for the finite-field theory it draws on live in the higher layers' *Mathlib counterparts, not in this library.