16.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).

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