inductive Hex.Nat.RhoStop : Type

Why a proper-factor search stopped without a factor.

• invalidInput : RhoStop

  n < 4: no proper-factor search is meaningful.

• exhausted : RhoStop

  A bounded search resource ran out: the restart allocation, a restart's bounded sampler or pair-draw allocation, or its Brent cycle budget. Includes prime inputs and composites for which no proper factor was found; makes no primality claim.

@[instance_reducible]

instance Hex.Nat.instReprRhoStop : Repr RhoStop

Equations

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

def Hex.Nat.instReprRhoStop.repr : RhoStop → Nat → Std.Format

Equations

• Hex.Nat.instReprRhoStop.repr Hex.Nat.RhoStop.invalidInput prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.Nat.RhoStop.invalidInput")).group prec✝
• Hex.Nat.instReprRhoStop.repr Hex.Nat.RhoStop.exhausted prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.Nat.RhoStop.exhausted")).group prec✝

@[instance_reducible]

instance Hex.Nat.instDecidableEqRhoStop : DecidableEq RhoStop

Equations

• Hex.Nat.instDecidableEqRhoStop x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Hex.Nat.RhoFailure : Type

A resumable failure, following the tree's randomized-search convention: the advanced state is returned even on failure, so callers can resume rather than accidentally reuse the same failed stream.

• stop : RhoStop

  Why the search stopped.

• attempts : Nat

  Restart attempts consumed by this failing search alone; callers running several searches accumulate their own totals. A draw that exhausts its bounded sampler or pair-draw allocation counts as the one restart it was trying to construct.

• rand : Rand

  The advanced generator state.

@[instance_reducible]

instance Hex.Nat.instReprRhoFailure : Repr RhoFailure

Equations

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

def Hex.Nat.instReprRhoFailure.repr : RhoFailure → Nat → Std.Format

Equations

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

inductive Hex.Nat.Internal.RhoDrawStop : Type

Why construction of one rho restart draw stopped.

• sample (error : RandError) : RhoDrawStop

  One coordinate's bounded natural-number sampler exhausted.

• pairs : RhoDrawStop

  Every admitted pair draw was fixed-point or globally degenerate.

@[instance_reducible]

instance Hex.Nat.Internal.instReprRhoDrawStop : Repr RhoDrawStop

Equations

• Hex.Nat.Internal.instReprRhoDrawStop = { reprPrec := Hex.Nat.Internal.instReprRhoDrawStop.repr }

def Hex.Nat.Internal.instReprRhoDrawStop.repr : RhoDrawStop → Nat → Std.Format

Equations

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

def Hex.Nat.Internal.sampleFuel : Nat

Bounded retries for one rejection-sampled natural number.

Equations

• Hex.Nat.Internal.sampleFuel = 64

def Hex.Nat.Internal.rhoPairFuel : Nat

Bounded pair draws within one semantic rho restart.

Equations

• Hex.Nat.Internal.rhoPairFuel = 8

def Hex.Nat.Internal.rhoRestartCap : Nat

Shared maximum rho restart allocation for current worklist consumers.

Equations

• Hex.Nat.Internal.rhoRestartCap = 8

def Hex.Nat.Internal.rhoRestartFuel (n innerFuel : Nat) : Nat

Effective Brent cycle budget for each restart: the caller's allocation capped by the input-scaled production budget.

Equations

• Hex.Nat.Internal.rhoRestartFuel n innerFuel = min (Hex.Nat.rhoInnerFuel✝ n) innerFuel

structure Hex.Nat.Internal.RhoSuccess : Type

A validated rho factor together with the exact number of restarts and the generator state after those restarts.

• factor : Nat

  Dynamically validated proper factor.

• attempts : Nat

  Restarts executed, including the successful restart.

• rand : Rand

  Generator state after all restart draws.

@[instance_reducible]

instance Hex.Nat.Internal.instReprRhoSuccess : Repr RhoSuccess

Equations

• Hex.Nat.Internal.instReprRhoSuccess = { reprPrec := Hex.Nat.Internal.instReprRhoSuccess.repr }

def Hex.Nat.Internal.instReprRhoSuccess.repr : RhoSuccess → Nat → Std.Format

Equations

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

structure Hex.Nat.Internal.RhoTrace : Type

Deterministic Brent instrumentation for route-level conformance tests.

• factor : Option Nat

  Candidate divisor returned by the restart, if any.

• steps : Nat

  Polynomial evaluations, including recovery replay.

• gcds : Nat

  Batched and recovery gcd computations.

• recoveries : Nat

  Whole-modulus batches replayed.

def Hex.Nat.Internal.rhoTrace (n c start fuel : Nat) : RhoTrace

Run one explicitly parameterized Brent restart and report its batching counters.

Equations

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

def Hex.Nat.Internal.rhoDrawTrace (n : Nat) (r : Rand) (drawFuel : Nat := sampleFuel) (pairFuel : Nat := rhoPairFuel) : Except (RhoDrawStop × Nat × Rand) (Nat × Nat × Nat × Rand)

Inspect an exact bounded restart draw. The error distinguishes sampler and pair-draw exhaustion and carries the pair-rejection count and exact state; sampler-internal rejections do not increment that count.

Equations

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

def Hex.Nat.Internal.rhoFactorCountedWith? (n : Nat) (r : Rand) (restarts innerFuel : Nat) : Except RhoFailure RhoSuccess

A dynamically validated proper-factor candidate by batched Brent rho, with its exact restart count.

Equations

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

def Hex.Nat.Internal.rhoFactorCounted? (n : Nat) (r : Rand) (fuel : Nat) : Except RhoFailure RhoSuccess

A counted rho search with the production per-restart cycle budget.

Equations

• Hex.Nat.Internal.rhoFactorCounted? n r fuel = Hex.Nat.Internal.rhoFactorCountedWith? n r fuel Hex.Nat.rhoInnerFuelCap✝

def Hex.Nat.rhoFactor? (n : Nat) (r : Rand) (fuel : Nat) : Except RhoFailure (Nat × Rand)

A dynamically validated proper-factor candidate by batched Brent rho. fuel bounds restart attempts. Each restart draws a fresh polynomial and starting point through bounded unbiased sampling, accumulates up to 32 differences per gcd, and replays a whole-modulus batch difference by difference. Its cycle budget is scaled to n^(1/4) and capped at 2^22 (see rhoInnerFuel), so exhaustion arrives rather than hangs when the smallest factor is out of rho's reach. Every success is validated (1 < d < n and d ∣ n) before it is returned, so randomness and fuel affect only whether a factor is found.

Equations

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

theorem Hex.Nat.Internal.rhoFactorCountedWith?_spec {n : Nat} {r : Rand} {restarts innerFuel : Nat} {success : RhoSuccess} (h : rhoFactorCountedWith? n r restarts innerFuel = Except.ok success) : 1 < success.factor ∧ success.factor < n ∧ success.factor ∣ n

A rho success under explicit restart and cycle budgets is a validated proper factor.

theorem Hex.Nat.Internal.rhoFactorCounted?_spec {n : Nat} {r : Rand} {fuel : Nat} {success : RhoSuccess} (h : rhoFactorCounted? n r fuel = Except.ok success) : 1 < success.factor ∧ success.factor < n ∧ success.factor ∣ n

A counted rho success is a validated proper factor.

theorem Hex.Nat.rhoFactor?_spec {n d : Nat} {r r' : Rand} {fuel : Nat} (h : rhoFactor? n r fuel = Except.ok (d, r')) : 1 < d ∧ d < n ∧ d ∣ n

The one theorem about the rho primitive: a success is a validated proper factor.

structure Hex.Nat.PartialFactors : Type

Candidate partial factorization: bases with positive exponents, and an unfactored residual. No primality and no completeness is claimed.

• factors : List (Nat × Nat)

  Claimed factor bases with exponents.

• residual : Nat

  The unfactored remainder.

def Hex.Nat.instReprPartialFactors.repr : PartialFactors → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Nat.instReprPartialFactors : Repr PartialFactors

Equations

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

structure Hex.Nat.FactorSearchResult : Type

Output of an untrusted partial-factor search used during certificate construction. The caller validates only the final PrimeCert; these fields carry search candidates and resumable resource accounting, not evidence.

• raw : PartialFactors

  Claimed factors and the unfactored residual.

• rand : Rand

  Generator state after every randomized attempt made by the search.

• attempts : Nat

  Semantic search attempts made by this invocation.

def Hex.Nat.instReprFactorSearchResult.repr : FactorSearchResult → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Nat.instReprFactorSearchResult : Repr FactorSearchResult

Equations

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

def Hex.Nat.Internal.trialExtractTrace (p m : Nat) : Nat × Nat

Exercise one trial-division extraction directly. Used by conformance to guard the high-valuation route independently of the full prime-table walk.

Equations

• Hex.Nat.Internal.trialExtractTrace p m = Hex.Nat.divOut✝ p (m.log2 + 1) m

structure Hex.Nat.PrimeCertBudget : Type

Pollard-rho work admitted at each partial-factor worklist entry during certificate search. This controls search resources only; every reported factor is still validated dynamically and every emitted certificate is checker-replayed.

• rhoRestarts : Nat

  Maximum Brent restarts at one worklist entry.

• rhoSteps : Nat

  Maximum Brent cycle steps per restart.

def Hex.Nat.instReprPrimeCertBudget.repr : PrimeCertBudget → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Nat.instReprPrimeCertBudget : Repr PrimeCertBudget

Equations

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

def Hex.Nat.instDecidableEqPrimeCertBudget.decEq (x✝ x✝¹ : PrimeCertBudget) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Hex.Nat.instDecidableEqPrimeCertBudget : DecidableEq PrimeCertBudget

Equations

• Hex.Nat.instDecidableEqPrimeCertBudget = Hex.Nat.instDecidableEqPrimeCertBudget.decEq

structure Hex.Nat.FactorSearchBudget : Type

Complete resource allocation for one untrusted partial-factor invocation. Nested primality checks receive primeFuel and primeBudget; the producer's own worklist receives factorFuel.

• primeBudget : PrimeCertBudget

  Rho allocation available to each nested primality-certificate search.

• primeFuel : Nat

  Attempt budget available to each nested primality-certificate search.

• factorFuel : Nat

  Worklist-entry budget available to the partial-factor producer.

@[instance_reducible]

instance Hex.Nat.instReprFactorSearchBudget : Repr FactorSearchBudget

Equations

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

def Hex.Nat.instReprFactorSearchBudget.repr : FactorSearchBudget → Nat → Std.Format

Equations

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

def Hex.Nat.instDecidableEqFactorSearchBudget.decEq (x✝ x✝¹ : FactorSearchBudget) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Hex.Nat.instDecidableEqFactorSearchBudget : DecidableEq FactorSearchBudget

Equations

• Hex.Nat.instDecidableEqFactorSearchBudget = Hex.Nat.instDecidableEqFactorSearchBudget.decEq

@[reducible, inline]

abbrev Hex.Nat.FactorSearch : Type

A bounded, resumable, untrusted partial-factor producer.

Equations

• Hex.Nat.FactorSearch = (Hex.Nat.FactorSearchBudget → Nat → Hex.Rand → Hex.Nat.FactorSearchResult)

def Hex.Nat.defaultPrimeCertBudget : PrimeCertBudget

The production certificate-search rho allocation used by the public API.

Equations

• Hex.Nat.defaultPrimeCertBudget = { rhoRestarts := Hex.Nat.rhoRestartBudget✝, rhoSteps := 1 <<< 22 }

def Hex.Nat.defaultFactorSearch : FactorSearch

The built-in partial-factor producer used by primeCert?.

Equations

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

inductive Hex.Nat.PrimeCertStop : Type

Why certificate search stopped without a certificate.

• composite : PrimeCertStop

  The input is provably composite (the size check, table completeness, or a Miller-Rabin witness); the failure is a verdict.

• exhausted : PrimeCertStop

  The search budget ran out; no primality claim either way.

def Hex.Nat.instReprPrimeCertStop.repr : PrimeCertStop → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Nat.instReprPrimeCertStop : Repr PrimeCertStop

Equations

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

@[instance_reducible]

instance Hex.Nat.instDecidableEqPrimeCertStop : DecidableEq PrimeCertStop

Equations

• Hex.Nat.instDecidableEqPrimeCertStop x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Hex.Nat.PrimeCertFailure : Type

A resumable certificate-search failure.

• stop : PrimeCertStop

  Why the search stopped.

• attempts : Nat

  Search attempts consumed by the complete invocation, including deterministic p−1 calls and successful subsearches completed before this failure.

• rand : Rand

  The advanced generator state.

def Hex.Nat.instReprPrimeCertFailure.repr : PrimeCertFailure → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Nat.instReprPrimeCertFailure : Repr PrimeCertFailure

Equations

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

structure Hex.Nat.PrimeDecisionFailure : Type

A resumable bounded-decision failure.

• attempts : Nat

  Attempts consumed by the complete certificate invocation (see PrimeCertFailure.attempts).

• rand : Rand

  The advanced generator state.

@[instance_reducible]

instance Hex.Nat.instReprPrimeDecisionFailure : Repr PrimeDecisionFailure

Equations

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

def Hex.Nat.instReprPrimeDecisionFailure.repr : PrimeDecisionFailure → Nat → Std.Format

Equations

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

structure Hex.Nat.NextPrimeFailure : Type

A resumable next-prime-search failure.

• rejectedCandidates : Nat

  Candidates conclusively rejected as composite before exhaustion. An undecided candidate is not counted.

• certAttempts : Nat

  Certificate-search attempts consumed by the undecided candidate, including deterministic p−1 calls. Table lookup, trial division, and Miller--Rabin work are not counted.

• rand : Rand

  The advanced generator state.

@[instance_reducible]

instance Hex.Nat.instReprNextPrimeFailure : Repr NextPrimeFailure

Equations

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

def Hex.Nat.instReprNextPrimeFailure.repr : NextPrimeFailure → Nat → Std.Format

Equations

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

def Hex.Nat.defaultPrimeFuel (n : Nat) : Nat

Default fuel for the bounded decision path: one certificate-construction level per input bit. Above the deterministic tiers, every recursive child that reaches construction is an odd factor from the product decomposition of n - 1; its complementary factor is at least two, so its bit length is strictly smaller. The complete table closes inputs below 17 bits without construction, leaving 16 spare units in this bound. This is not a claim that bounded factor or witness search finds every available certificate.

Equations

• Hex.Nat.defaultPrimeFuel n = n.log2 + 1

def Hex.Nat.Internal.witnessDrawTrace (n : Nat) (r : Rand) (drawFuel : Nat := sampleFuel) : Except RandError (Nat × Rand)

Inspect one bounded witness-base draw, including its exact advanced state.

Equations

• Hex.Nat.Internal.witnessDrawTrace n r drawFuel = Hex.Nat.witnessDraw✝ n r drawFuel

def Hex.Nat.Internal.witnessSearchTrace (n q : Nat) (r : Rand) (candidates : Nat) (drawFuel : Nat := sampleFuel) : Except PrimeCertFailure (Nat × Nat × Rand)

Inspect bounded witness search while retaining its exact candidate count and final state. The optional sampler fuel is for route-level conformance.

Equations

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

structure Hex.Nat.Internal.PrimeCertSuccess (n : Nat) : Type

A checked primality certificate together with the exact number of p−1 calls, randomized rho restarts, and witness candidates used to construct it.

• cert : CheckedPrimeCert n

  Kernel-replayable checked certificate.

• attempts : Nat

  Search attempts used throughout the recursive construction.

• rand : Rand

  Generator state after those attempts.

def Hex.Nat.Internal.primeCertCountedUsing? (factor : FactorSearch) (budget : PrimeCertBudget) (n : Nat) (r : Rand) (fuel : Nat) : Except PrimeCertFailure (PrimeCertSuccess n)

Bounded certificate search with an explicit rho allocation, retaining exact successful-attempt metering.

Equations

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

def Hex.Nat.Internal.primeCertCountedWith? (budget : PrimeCertBudget) (n : Nat) (r : Rand) (fuel : Nat) : Except PrimeCertFailure (PrimeCertSuccess n)

Bounded certificate search with an explicit rho allocation, retaining exact successful-attempt metering and using the built-in factor producer.

Equations

• Hex.Nat.Internal.primeCertCountedWith? budget n r fuel = Hex.Nat.Internal.primeCertCountedUsing? Hex.Nat.defaultFactorSearch budget n r fuel

def Hex.Nat.Internal.primeCertCounted? (n : Nat) (r : Rand) (fuel : Nat) : Except PrimeCertFailure (PrimeCertSuccess n)

Bounded certificate search retaining exact successful-attempt metering.

Equations

• Hex.Nat.Internal.primeCertCounted? n r fuel = Hex.Nat.Internal.primeCertCountedWith? Hex.Nat.defaultPrimeCertBudget n r fuel

def Hex.Nat.primeCertWith? (factor : FactorSearch) (n : Nat) (r : Rand) (fuel : Nat) : Except PrimeCertFailure (CheckedPrimeCert n × Rand)

Bounded certificate search using an explicitly supplied, untrusted partial-factor producer. Only the returned CheckedPrimeCert is accepted; the producer's factors, accounting, and random state remain search data.

Equations

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

def Hex.Nat.primeCert? (n : Nat) (r : Rand) (fuel : Nat) : Except PrimeCertFailure (CheckedPrimeCert n × Rand)

Bounded certificate search. A success is a CheckedPrimeCert, so a certificate for one number can never answer a request about another; a .composite failure is a verdict (see primeCert?_composite); an .exhausted failure makes no claim and carries the advanced state.

Equations

• Hex.Nat.primeCert? n r fuel = match Hex.Nat.Internal.primeCertCounted? n r fuel with | Except.error failure => Except.error failure | Except.ok success => Except.ok (success.cert, success.rand)

theorem Hex.Nat.Internal.primeCertCountedUsing?_composite {factor : FactorSearch} {budget : PrimeCertBudget} {n : Nat} {r : Rand} {fuel : Nat} {f : PrimeCertFailure} (hresult : primeCertCountedUsing? factor budget n r fuel = Except.error f) (hstop : f.stop = PrimeCertStop.composite) : ¬Prime n

A counted .composite failure is a verdict for every factor producer and resource allocation because only the fixed size, table, and Miller--Rabin tiers can emit that stop reason.

theorem Hex.Nat.Internal.primeCertCountedWith?_composite {budget : PrimeCertBudget} {n : Nat} {r : Rand} {fuel : Nat} {f : PrimeCertFailure} (hresult : primeCertCountedWith? budget n r fuel = Except.error f) (hstop : f.stop = PrimeCertStop.composite) : ¬Prime n

A budgeted counted .composite failure under the built-in factor producer is a verdict.

theorem Hex.Nat.Internal.primeCertCounted?_composite {n : Nat} {r : Rand} {fuel : Nat} {f : PrimeCertFailure} (hresult : primeCertCounted? n r fuel = Except.error f) (hstop : f.stop = PrimeCertStop.composite) : ¬Prime n

A counted .composite failure under the default allocation is a verdict: the input is not prime.

theorem Hex.Nat.primeCertWith?_composite {factor : FactorSearch} {n : Nat} {r : Rand} {fuel : Nat} {f : PrimeCertFailure} (hresult : primeCertWith? factor n r fuel = Except.error f) (hstop : f.stop = PrimeCertStop.composite) : ¬Prime n

A .composite failure is a verdict for every supplied factor producer.

theorem Hex.Nat.primeCert?_composite {n : Nat} {r : Rand} {fuel : Nat} {f : PrimeCertFailure} (hresult : primeCert? n r fuel = Except.error f) (hstop : f.stop = PrimeCertStop.composite) : ¬Prime n

A .composite failure is a verdict: the input is not prime. Justified by size, table completeness, or a failed Miller-Rabin base; never by anything the untrusted search merely failed to do.

def Hex.Nat.isPrimeTrialThreshold : Nat

After Miller--Rabin filtering, exact trial division handles inputs from primeTableBound to 6000000. This round boundary lies between the measured Cunningham-chain rungs where trial last wins (near 5 · 10^6) and certificate search first wins (near 6 · 10^6).

Equations

• Hex.Nat.isPrimeTrialThreshold = 6000000

def Hex.Nat.isPrime? (n : Nat) (r : Rand) (fuel : Nat) : Except PrimeDecisionFailure (Bool × Rand)

The bounded decision: table below primeTableBound, Miller--Rabin composite filtering, exact trial division below isPrimeTrialThreshold, then certificate search. A failed base or a table/trial miss returns a certified false; an accepted certificate returns true; an exhausted search is an error rather than an unbounded computation.

Equations

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

theorem Hex.Nat.isPrime?_spec {n : Nat} {r : Rand} {fuel : Nat} {b : Bool} {r' : Rand} (h : isPrime? n r fuel = Except.ok (b, r')) : b = true ↔ Prime n

Every successful bounded decision is exact.

def Hex.Nat.isPrime (n : Nat) : Bool

The pure total convenience decision: the bounded path from the reproducible seed, with exact trial division as the fallback if that path exhausts its fuel, which is what makes the iff unconditional. Callers that need a real time bound and resumable state use isPrime?.

Equations

• Hex.Nat.isPrime n = match Hex.Nat.isPrime? n (Hex.Rand.ofSeed n) (Hex.Nat.defaultPrimeFuel n) with | Except.ok (b, snd) => b | Except.error a => Hex.Nat.isPrimeTrial n

theorem Hex.Nat.isPrime_iff {n : Nat} : isPrime n = true ↔ Prime n

The total decision is exact.

def Hex.Nat.nextPrime? (n : Nat) (r : Rand) (fuel : Nat) : Except NextPrimeFailure (Nat × Rand)

Fuel-bounded least-prime-above search: a total form needs Euclid's theorem, which this tree does not carry Mathlib-free, so exhaustion is reported with separate counts for conclusively rejected candidates and certificate-search attempts, plus the exact advanced state. On failure, rejectedCandidates = fuel means the candidate window was exhausted; otherwise the undecided candidate is n + 1 + rejectedCandidates.

Equations

• Hex.Nat.nextPrime? n r fuel = Hex.Nat.nextPrimeGo✝ fuel fuel (n + 1) 0 r

theorem Hex.Nat.nextPrime?_spec {n : Nat} {r : Rand} {fuel p : Nat} {r' : Rand} (h : nextPrime? n r fuel = Except.ok (p, r')) : n < p ∧ Prime p ∧ ∀ (q : Nat), n < q → q < p → ¬Prime q

A successful search returns the least prime above n.