def Hex.ECPP.compactCertTerm : Lean.ParserDescr

A saved elliptic curve primality certificate, encoded as PARI rows and a HexPrimality certificate for the last prime. Use ecpp using (ecpp_cert% "rows" using lastPrimeCertificate) to prove the recorded integer prime. This notation reconstructs the certificate's arithmetic witnesses; it does not invoke PARI or repeat curve search.

Equations

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

def Hex.ECPP.elabCompactCert : Lean.Elab.Term.TermElab

Read a saved certificate's rows and last-prime certificate, reconstruct the modular inverses, and expose the resulting constructor data for proof checking. Reject invalid input or exceeded certificate limits.

Equations

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

def Hex.ECPP.terminalCert : Cert → Nat.PrimeCert

Extract the HexPrimality certificate that proves the last prime in an ECPP certificate's chain.

Equations

• Hex.ECPP.terminalCert (Hex.ECPP.Cert.base leaf) = leaf
• Hex.ECPP.terminalCert (Hex.ECPP.Cert.step n a b x_1 y discrInv inverses child) = Hex.ECPP.terminalCert child

def Hex.ECPP.compactSyntax (source : String) (cert : Cert) : Lean.MetaM Lean.Term

Render saved curves and points with their last-prime certificate as an ecpp_cert% expression. Modular inverses are reconstructed when that saved expression is elaborated, so they need not all appear in the source text.

Equations

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

def Hex.ECPP.exportCertificate (mod decl : Lean.TSyntax `ident) (term : Lean.Term) (generator : ℕ → Lean.MetaM (String × Cert)) : Lean.Elab.Command.CommandElabM Unit

Common explicit export for certificate producers. Validate the destination before search, then create it exclusively after kernel-checked generation.

Equations

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