structure Hex.Nat.ConstructionBudget : Type

Finite, opt-in certificate construction resources. ECM is disabled on this Mathlib-free core route (zero curves and no ECM bounds).

• maxBits : Nat
• maxDepth : Nat
• maxAttempts : Nat
• factor : FactorSearchBudget
• witnessBases : List Nat
• randomWitnesses : Nat
• maxFactors : Nat
• maxSubsets : Nat
• maxSieveBound : Nat

def Hex.Nat.instReprConstructionBudget.repr : ConstructionBudget → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Nat.instReprConstructionBudget : Repr ConstructionBudget

Equations

• Hex.Nat.instReprConstructionBudget = { reprPrec := Hex.Nat.instReprConstructionBudget.repr }

def Hex.Nat.instDecidableEqConstructionBudget.decEq (x✝ x✝¹ : ConstructionBudget) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Hex.Nat.instDecidableEqConstructionBudget : DecidableEq ConstructionBudget

Equations

• Hex.Nat.instDecidableEqConstructionBudget = Hex.Nat.instDecidableEqConstructionBudget.decEq

def Hex.Nat.constructionBudget : ConstructionBudget

The reproducible construction profile used by primality?.

Equations

• Hex.Nat.constructionBudget = { }

structure Hex.Nat.Construction.Failureextends Hex.Nat.PrimeCertFailure : Type

Construction exhaustion with an unresolved recursive subject. The ordinary search failure API remains available through run.

• stop : PrimeCertStop
• attempts : Nat
• rand : Rand
• events : List FactorEvent
• obligation : Option Nat

def Hex.Nat.Construction.factorSearch : FactorSearch

Table division followed by the explicitly budgeted smooth/rho worklist. Every unresolved component is retained in the residual.

Equations

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

def Hex.Nat.Construction.sufficient (budget : ConstructionBudget) (n F : Nat) : Bool

Cheap size and discriminant screening before any recursive certification. The public checker validates these computations again on the final literal.

Equations

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

def Hex.Nat.Construction.runTraced (n : Nat) (r : Rand) (budget : ConstructionBudget := constructionBudget) (factor : FactorSearch := factorSearch) : Except Failure (Internal.PrimeCertSuccess n)

Construct and self-check the exact certificate to be reified. Factor data, subset estimates and witnesses are untrusted; every success passes checkPrime. A malformed producer can only prevent certificate construction.

Equations

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

def Hex.Nat.Construction.run (n : Nat) (r : Rand) (budget : ConstructionBudget := constructionBudget) (factor : FactorSearch := factorSearch) : Except PrimeCertFailure (Internal.PrimeCertSuccess n)

Construct and self-check a certificate with the ordinary search failure API.

Equations

• Hex.Nat.Construction.run n r budget factor = match Hex.Nat.Construction.runTraced n r budget factor with | Except.ok s => Except.ok s | Except.error f => Except.error f.toPrimeCertFailure

def Hex.Nat.Construction.retryable (n : Nat) (budget : ConstructionBudget) (first : Failure) : Bool

Whether exhaustion permits another provider under the original shared allowance.

Equations

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

def Hex.Nat.Construction.retry (n : Nat) (budget : ConstructionBudget) (first : Failure) (factor : FactorSearch) : Except Failure (Internal.PrimeCertSuccess n)

One complete bounded retry after exhaustion. Repeated work is charged, random state advances, and events remain in execution order.

Equations

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