@[reducible, inline]

abbrev Hex.Conway.EntrySource.CertData : Type

Serialized Rabin certificate: the prime, the degree, the Frobenius pow chain, and the Bezout witness pairs, all as canonical Nat representatives.

Equations

• Hex.Conway.EntrySource.CertData = (Nat × Nat × List (List Nat) × List (List Nat × List Nat))

def Hex.Conway.EntrySource.entryCertData (p : Nat) (coeffs : List Nat) : Option CertData

Compute the Rabin irreducibility certificate for C(p, n) from its coefficient list, serialized to plain Nat data.

Returns none when the modulus is out of ZMod64 range, when the coefficient list is not monic, or when the polynomial fails Rabin's test, which for a correctly transcribed Conway entry means the transcription is wrong.

Equations

• One or more equations did not get rendered due to their size.

def Hex.Conway.EntrySource.entryCertValidates (p : Nat) (coeffs : List Nat) (cert : CertData) : Bool

Re-check a generated certificate the way the committed decide will.

This is the predicate used by the inspection block. A false rejects the certificate; true checks its arithmetic in compiled code but does not establish that kernel replay fits the elaboration budget. The complete generator uses the proved-equivalent binary checker in HexConway.Power.

Equations

• One or more equations did not get rendered due to their size.

def Hex.Conway.EntrySource.renderCoeffs (p : Nat) (coeffs : List Nat) : String

Render a coefficient list as the FpPoly literal the committed entries use: the first residue carries the type ascription that fixes p, and the empty list needs the ascription on the array instead.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Conway.EntrySource.renderCoeffs p [] = toString "FpPoly.ofCoeffs (#[] : Array (ZMod64 " ++ toString p ++ toString "))"

def Hex.Conway.EntrySource.hitLemma (p n : Nat) (coeffs : List Nat) (name : String) : String

Render the table-hit lemma, whose closing match needs one rfl arm per stored coefficient plus a catch-all for the positions above the degree.

Equations

• One or more equations did not get rendered due to their size.

def Hex.Conway.EntrySource.apiBlock (p n : Nat) (coeffs : List Nat) (name : String) : String

Render the coefficient-list transports and the SupportedEntry witness that HexConway.Api carries for each committed entry.

Equations

• One or more equations did not get rendered due to their size.

def Hex.Conway.EntrySource.entryBlock (p n : Nat) (coeffs : List Nat) (cert : CertData) : String

Render the per-entry source block for (p, n): the table-side literal with its monic and degree lemmas, then the certificate side with its kernel check and the irreducibility theorem.

Equations

• One or more equations did not get rendered due to their size.

def Hex.Conway.EntrySource.conwayEntrySource : Lean.ParserDescr

Print the per-entry source block for a Conway pair in the committed cache.

Takes only the pair. The coefficients are read from the cache row for that pair rather than supplied by the caller, so the emitted block cannot be labelled C(p, n) while holding some other polynomial. That distinction matters because Tier 1 proves only that a committed entry is monic, irreducible, and of the requested degree; nothing in Lean says it is the Conway polynomial, so a mislabelled entry would typecheck.

Refresh the expansion input with scripts/conway/import_source.py if needed, and check whether the requested source entry is available. The shared factorization corpus cache is separate.

Equations

• One or more equations did not get rendered due to their size.

def Hex.Conway.EntrySource.elabEntrySource : Lean.Elab.Command.CommandElab

Equations

• One or more equations did not get rendered due to their size.