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

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

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.

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

The main entry point composes the two: it looks up the coefficient list and, on a hit, builds the polynomial. The table has 594 verified entries:

• characteristic 2, degrees 1–16;

• characteristics 3, 5 and 7, degrees 1–8;

• characteristics 11 and 13, degrees 1–6;

• other primes below 300, degrees 1–4;

• primes between 300 and 1000, degrees 1–3.

These ranges have no holes and contain every positive divisor of each supported degree. Every entry has irreducibility and primitivity proofs, and the 522 proper-divisor pairs have compatibility proofs. Other pairs return none. The scope is selected by measuring a complete rebuild against the five-minute ceiling; the broader source cache does not by itself establish verified support.

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)