def Hex.PrimalityTactic.searchExtensionVersion : Nat

ABI version of the downstream factor-search registration boundary.

Equations

• Hex.PrimalityTactic.searchExtensionVersion = 3

structure Hex.PrimalityTactic.SearchExtension : Type

One downstream partial-factor producer available to elaboration-time certificate search. The version is checked before the function is used.

• version : Nat

  Version of the extension ABI implemented by this registration.

• factorName : Lean.Name

  Fully qualified name of the registered partial-factor producer.

def Hex.PrimalityTactic.searchExtensionNames : List Lean.Name

Well-known search-extension constants, checked in deterministic order. Adding or reordering an entry requires a HexPrimality release.

Equations

• Hex.PrimalityTactic.searchExtensionNames = [`HexIntFactor.PrimalityTactic.extension]

def Hex.PrimalityTactic.searchExtensions : Lean.MetaM (List SearchExtension)

Registered factor-search extensions present in the environment. Each declaration's type and ABI version are checked before deterministic dispatch.

Equations

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

def Hex.PrimalityTactic.constructionExtensionVersion : Nat

ABI version of providers selected before bounded certificate construction.

Equations

• Hex.PrimalityTactic.constructionExtensionVersion = 2

structure Hex.PrimalityTactic.ConstructionExtension : Type

A downstream default construction provider, separate from ordinary search.

• version : Nat

  Version of the bounded-construction registration ABI.

• factorName : Lean.Name

  An ordinary definition at Hex.Nat.FactorSearch.

def Hex.PrimalityTactic.constructionExtensionNames : List Lean.Name

Fixed discovery order. The first present registration supplies the factor provider for the entire construction. Changes require a HexPrimality release.

Equations

• Hex.PrimalityTactic.constructionExtensionNames = [`HexIntFactor.PrimalityTactic.constructionExtension]

def Hex.PrimalityTactic.constructionExtension? (n : Lean.Name) : Lean.MetaM (Option ConstructionExtension)

Validate a present registration before evaluating its factor provider. Absence is allowed; malformed registrations are errors, not silent skips.

Equations

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

def Hex.PrimalityTactic.construct (n : Nat) (budget : Nat.ConstructionBudget) : Lean.MetaM (Except Nat.Construction.Failure (Nat.Internal.PrimeCertSuccess n) × List (Lean.Name × Nat))

Select the first registered construction provider before searching, or the core provider when none is imported. Table primes, composites, invalid sizes and zero allowances return without inspecting registrations. A single run shares its allocation across factoring, children and witnesses.

Equations

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

def Hex.PrimalityTactic.reflTrue : Lean.Expr

Eq.refl true as a raw proof slot: the kernel verifies the reified Bool equation by reduction alone.

Equations

• Hex.PrimalityTactic.reflTrue = Lean.mkApp2 (Lean.mkConst `Eq.refl [Lean.Level.one]) (Lean.mkConst `Bool) (Lean.mkConst `Bool.true)

def Hex.PrimalityTactic.reifyPrimeCert : Nat.PrimeCert → Lean.Expr

Reify a certificate as constructor applications over Nat literals. Pure data with no proof slots, so the reifier is total and the kernel obligations all live in the one Eq.refl true slot of the wrapper.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PrimalityTactic.reifyPrimeCert (Hex.Nat.PrimeCert.small n) = Lean.mkApp (Lean.mkConst `Hex.Nat.PrimeCert.small) (Lean.mkNatLit n)
• Hex.PrimalityTactic.reifyPrimeCert (Hex.Nat.PrimeCert.pock n factors) = Lean.mkApp2 (Lean.mkConst `Hex.Nat.PrimeCert.pock) (Lean.mkNatLit n) (Hex.PrimalityTactic.reifyFactors factors)

def Hex.PrimalityTactic.reifyFactors : List (Nat × Nat × Nat.PrimeCert) → Lean.Expr

Reify a factor list.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PrimalityTactic.reifyFactors [] = Lean.mkApp (Lean.mkConst `List.nil [Lean.Level.zero]) Hex.PrimalityTactic.tripleTy✝

def Hex.PrimalityTactic.checkClosed (tactic : String) (e : Lean.Expr) : Lean.MetaM Unit

Reject open terms: the search and the kernel replay both need a closed numeral.

Equations

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

def Hex.PrimalityTactic.primalityBitBudget : Nat

Supported bit-length ceiling for every elaboration-time certificate route. The 512-bit boundary is the largest measured fresh-module rung; changing it requires new end-to-end search, reification, and kernel-replay evidence.

Equations

• Hex.PrimalityTactic.primalityBitBudget = 512

def Hex.PrimalityTactic.primalityFuelBudget : Nat

Maximum recursive fuel passed to elaboration-time certificate search. The settled default is one unit per input bit, so this is deliberately the same quantity as the supported input ceiling. Keeping the definitions linked prevents one policy boundary from changing without the other.

Equations

• Hex.PrimalityTactic.primalityFuelBudget = Hex.PrimalityTactic.primalityBitBudget

def Hex.PrimalityTactic.primalityRhoRestartBudget : Nat

Maximum Brent restarts at one partial-factor worklist entry on every elaboration-time certificate route.

Equations

• Hex.PrimalityTactic.primalityRhoRestartBudget = 2

def Hex.PrimalityTactic.primalityRhoStepBudget : Nat

Maximum Brent cycle steps per restart on every elaboration-time certificate route.

Equations

• Hex.PrimalityTactic.primalityRhoStepBudget = 1 <<< 15

def Hex.PrimalityTactic.primalitySearchBudget : Nat.PrimeCertBudget

The explicit rho allocation shared by every elaboration-time route.

Equations

• Hex.PrimalityTactic.primalitySearchBudget = { rhoRestarts := Hex.PrimalityTactic.primalityRhoRestartBudget, rhoSteps := Hex.PrimalityTactic.primalityRhoStepBudget }

def Hex.PrimalityTactic.primalityFuel (n : Nat) : Nat

The fuel selected by every elaboration-time certificate route.

Equations

• Hex.PrimalityTactic.primalityFuel n = min (Hex.Nat.defaultPrimeFuel n) Hex.PrimalityTactic.primalityFuelBudget

def Hex.PrimalityTactic.withinPrimalityBudget (n : Nat) : Bool

Whether an input is admitted by the common elaboration policy.

Equations

• Hex.PrimalityTactic.withinPrimalityBudget n = decide (n.log2 + 1 ≤ Hex.PrimalityTactic.primalityBitBudget)

def Hex.PrimalityTactic.checkPrimalityPolicy (tactic : String) (n : Nat) : Lean.MetaM Unit

Enforce the common input-size policy before any certificate search.

Equations

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

def Hex.PrimalityTactic.throwPrimalityExhausted {α : Type} (tactic : String) (n attempts fuel : Nat) : Lean.MetaM α

Report bounded-search exhaustion without inviting an unbounded fallback.

Equations

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

def Hex.PrimalityTactic.provePrimeWith (head : Lean.Name) (tactic : String) (n : Nat) (nE : Lean.Expr) : Lean.MetaM Lean.Expr

Run the certificate search and emit the checked proof term with head applied to the subject, the reified certificate, and the Eq.refl true slot: prime_of_checkPrimeAt here, the companion's Nat.Prime-flavoured wrapper there. The search result is self-checked with the same compiled checkPrime the kernel will replay before anything is emitted.

Equations

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

def Hex.PrimalityTactic.provePrime (tactic : String) (n : Nat) (nE : Lean.Expr) : Lean.MetaM Lean.Expr

provePrimeWith at the Mathlib-free wrapper: the proof term for Hex.Nat.Prime n.

Equations

• Hex.PrimalityTactic.provePrime tactic n nE = Hex.PrimalityTactic.provePrimeWith `Hex.Nat.prime_of_checkPrimeAt tactic n nE

def Hex.PrimalityTactic.elabPrimalityArgument (t : Lean.Syntax) : Lean.Elab.TermElabM Lean.Expr

Elaborate a primality argument to its numeral and proof.

Equations

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

def Hex.PrimalityTactic.primalityTerm : Lean.ParserDescr

primality n elaborates to a proof of Hex.Nat.Prime n for a literal n.

Equations

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

def Hex.PrimalityTactic.elabPrimality : Lean.Elab.Term.TermElab

Elaborator for the Mathlib-free primality n term syntax.

Equations

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

def Hex.PrimalityTactic.goalPrime (goal : Lean.MVarId) : Lean.Elab.Tactic.TacticM Bool

Try to close a goal of the form Hex.Nat.Prime e; return false when the goal has a different shape.

Equations

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

def Hex.PrimalityTactic.primalityTac : Lean.ParserDescr

Tactic forms of primality: bare primality closes a Hex.Nat.Prime e goal; primality n adds the proof as this; primality h : n names it h.

Equations

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

def Hex.PrimalityTactic.evalPrimalityTac : Lean.Elab.Tactic.Tactic

Evaluator for the Mathlib-free primality tactic forms.

Equations

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

def Hex.PrimalityTactic.certificateSyntax (cert : Nat.PrimeCert) : Lean.MetaM Lean.Term

Render a literal using the same expression reifier as ordinary proof emission. Full names and fixed pretty-printing options make the suggestion independent of namespace openings and display settings.

Equations

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

def Hex.PrimalityTactic.constructionDescription (b : Nat.ConstructionBudget) (provider : Option String := none) (registered : Bool := false) : String

The complete finite construction resource description used in diagnostics.

def Hex.PrimalityTactic.suppliedCertificate (stx : Lean.Term) (n : Nat) : Lean.Elab.TermElabM Nat.PrimeCert

Evaluate an explicitly supplied, closed producer as untrusted code. Only its literal result reaches the proof; neither the producer nor its imports are needed to replay the suggestion.

Equations

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

def Hex.PrimalityTactic.primalitySuggestFactorTac : Lean.ParserDescr

Explicitly select an untrusted factor provider for bounded construction.

Equations

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

def Hex.PrimalityTactic.primalitySuggestTac : Lean.ParserDescr

Construct a reusable certificate with an optional total attempt limit.

Equations

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

def Hex.PrimalityTactic.primalitySuggestUsingTac : Lean.ParserDescr

Check and render an explicitly selected closed certificate producer.

Equations

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

def Hex.PrimalityTactic.suggestPrime (predicate head : Lean.Name) (stx : Lean.Syntax) : Lean.Elab.Tactic.TacticM Unit

Shared goal handler for core and companion primality? registrations.

Equations

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

def Hex.PrimalityTactic.evalPrimalitySuggest : Lean.Elab.Tactic.Tactic

Core certificate-literal suggestion handler.

Equations

• Hex.PrimalityTactic.evalPrimalitySuggest = Hex.PrimalityTactic.suggestPrime `Hex.Nat.Prime `Hex.Nat.prime_of_checkPrimeAt