def Hex.PrimalityTactic.searchExtensionVersion : Nat

ABI version of the downstream factor-search registration boundary.

Equations

• Hex.PrimalityTactic.searchExtensionVersion = 1

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