16.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 supported coverage is p ∈ {2, 3, 5, 7, 11, 13} and n ∈ {1, …, 6}. Every other pair returns none rather than triggering Tier 2 compatibility checks or Tier 3 search.

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)