fix(hex-primality): preserve next-prime search work accounting

HexPrimality/SPEC/hex-primality.md

@@ -777,8 +777,9 @@ structure PrimeDecisionFailure where
   rand     : Rand
 
 structure NextPrimeFailure where
-  attempts : Nat
-  rand     : Rand
+  rejectedCandidates : Nat
+  certAttempts       : Nat
+  rand               : Rand
 
 def defaultPrimeFuel (n : Nat) : Nat
 
@@ -878,8 +879,20 @@ this tree has neither Mathlib-free; an earlier draft of this SPEC
 declared `nextPrime : Nat → Nat` with no account of either. Adding
 Euclid would make the total form available and is not on any consumer's
 critical path, so `NextPrimeFailure` reports exhaustion with the attempt
-count and advanced state. The theorem records that a success is the
-*least* such prime.
+counts and advanced state. The units are separate: `rejectedCandidates`
+counts only candidates conclusively proved composite, while `certAttempts`
+counts randomized certificate-search attempts consumed by the candidate
+whose decision exhausted. An undecided candidate is not included in
+`rejectedCandidates`. If the candidate window itself is exhausted,
+`certAttempts` is zero. In either case `rand` is the exact state after all
+reported randomized work, so a caller can replay or resume without losing
+work. Deterministic table lookup, trial division, and Miller--Rabin filtering
+do not contribute to `certAttempts`; in particular, every conclusively rejected
+candidate leaves both this count and `rand` unchanged. A failure with
+`rejectedCandidates = fuel` exhausted the whole candidate window. Otherwise
+the undecided candidate is `n + 1 + rejectedCandidates`, so the two failure
+modes and the resumption point are recoverable from the call and its failure.
+The theorem records that a success is the *least* such prime.
 
 `primeCert?` distinguishes `PrimeCertStop.composite`, justified by the size
 check, table completeness, or a failed Miller-Rabin base, from `.exhausted`,

HexPrimality/Search.lean

@@ -629,9 +629,13 @@ deriving Repr
 
 /-- A resumable next-prime-search failure. -/
 structure NextPrimeFailure where
-  /-- Candidates conclusively rejected before the failure; the candidate
-  whose decision failed is not counted. -/
-  attempts : Nat
+  /-- Candidates conclusively rejected as composite before exhaustion. An
+  undecided candidate is not counted. -/
+  rejectedCandidates : Nat
+  /-- Randomized certificate-search attempts consumed by the undecided
+  candidate. Deterministic table, trial-division, and Miller--Rabin work is
+  not counted. -/
+  certAttempts : Nat
   /-- The advanced generator state. -/
   rand : Rand
 deriving Repr
@@ -1017,16 +1021,17 @@ theorem isPrime_iff {n : Nat} : isPrime n = true ↔ Prime n := by
 
 private def nextPrimeGo (certFuel : Nat) :
     Nat → Nat → Nat → Rand → Except NextPrimeFailure (Nat × Rand)
-  | 0, _, attempts, r => .error ⟨attempts, r⟩
-  | steps + 1, m, attempts, r =>
+  | 0, _, rejectedCandidates, r => .error ⟨rejectedCandidates, 0, r⟩
+  | steps + 1, m, rejectedCandidates, r =>
       match isPrime? m r certFuel with
-      | .error f => .error ⟨attempts, f.rand⟩
+      | .error f => .error ⟨rejectedCandidates, f.attempts, f.rand⟩
       | .ok (true, r') => .ok (m, r')
-      | .ok (false, r') => nextPrimeGo certFuel steps (m + 1) (attempts + 1) r'
+      | .ok (false, r') =>
+          nextPrimeGo certFuel steps (m + 1) (rejectedCandidates + 1) r'
 
 private theorem nextPrimeGo_spec (certFuel : Nat) :
-    ∀ (steps m attempts : Nat) (r : Rand) {p : Nat} {r' : Rand},
-      nextPrimeGo certFuel steps m attempts r = .ok (p, r') →
+    ∀ (steps m rejectedCandidates : Nat) (r : Rand) {p : Nat} {r' : Rand},
+      nextPrimeGo certFuel steps m rejectedCandidates r = .ok (p, r') →
       m ≤ p ∧ Prime p ∧ ∀ q, m ≤ q → q < p → ¬ Prime q := by
   intro steps
   induction steps with
@@ -1059,7 +1064,10 @@ private theorem nextPrimeGo_spec (certFuel : Nat) :
 
 /-- 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 the attempt count and advanced state. -/
+reported with separate counts for conclusively rejected candidates and
+randomized 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`. -/
 def nextPrime? (n : Nat) (r : Rand) (fuel : Nat) :
     Except NextPrimeFailure (Nat × Rand) :=
   nextPrimeGo fuel fuel (n + 1) 0 r

conformance/HexPrimality/Conformance.lean

@@ -30,6 +30,8 @@ Covered operations:
 Covered properties:
 - the total decision agrees with trial division on an initial segment
 - a `.composite` certificate-search verdict never contradicts `isPrime`
+- next-prime exhaustion separates rejected candidates from certificate work
+  and returns the exact advanced random state
 - accepted certificates replay; each rejection reason rejects
 - the committed table window and the runtime segment listing agree
 - the small sieve agrees with trial division on every represented index
@@ -282,10 +284,55 @@ private def rhoRecoveryTrace : Hex.Nat.Internal.RhoTrace :=
 #guard (primesIn 99950 100050).toList.all fun p =>
   isTablePrime p == decide (p < 100000)
 
--- Next-prime search across the table edge.
-#guard (match nextPrime? 99991 (Hex.Rand.ofSeed 0) 64 with
-        | .ok (p, _) => p == 100003
-        | .error _ => false)
+-- Next-prime success returns the least prime across the table, trial, and
+-- certificate tiers.
+#guard (match nextPrime? 90 (Hex.Rand.ofSeed 0) 8 with
+  | .ok (p, _) => p == 97
+  | .error _ => false)
+#guard (match nextPrime? 99991 (Hex.Rand.ofSeed 0) 16 with
+  | .ok (p, _) => p == 100003
+  | .error _ => false)
+#guard (match nextPrime? 10000000 (Hex.Rand.ofSeed 0) 32,
+    isPrime? 10000019 (Hex.Rand.ofSeed 0) 32 with
+  | .ok (p, r), .ok (true, directRand) => p == 10000019 && r == directRand
+  | _, _ => false)
+
+-- Candidate-window exhaustion counts every proved-composite candidate but no
+-- certificate attempts, and deterministic decisions leave the seed unchanged.
+#guard (match nextPrime? 90 (Hex.Rand.ofSeed 0) 6 with
+  | .error failure =>
+      failure.rejectedCandidates == 6 && failure.certAttempts == 0 &&
+        failure.rand == Hex.Rand.ofSeed 0
+  | .ok _ => false)
+
+-- Certificate-tier composite verdicts also consume no randomized work, so
+-- exhausting a window of them leaves the seed unchanged.
+#guard (match nextPrime? 10000000 (Hex.Rand.ofSeed 0) 4 with
+  | .error failure =>
+      failure.rejectedCandidates == 4 && failure.certAttempts == 0 &&
+        failure.rand == Hex.Rand.ofSeed 0
+  | .ok _ => false)
+
+-- The first candidate is undecided after nonzero randomized work. Its
+-- certificate attempts and exact advanced state are retained, but it is not
+-- counted as conclusively rejected.
+#guard (match nextPrime? 1000000006 (Hex.Rand.ofSeed 3) 2,
+    isPrime? 1000000007 (Hex.Rand.ofSeed 3) 2 with
+  | .error failure, .error decisionFailure =>
+      failure.rejectedCandidates == 0 && failure.certAttempts == 7 &&
+        failure.certAttempts == decisionFailure.attempts &&
+        failure.rand == decisionFailure.rand
+  | _, _ => false)
+
+-- A preceding deterministic composite and a later undecided candidate retain
+-- both nonzero units without counting the undecided candidate as rejected.
+#guard (match nextPrime? 1000000005 (Hex.Rand.ofSeed 3) 2,
+    isPrime? 1000000007 (Hex.Rand.ofSeed 3) 2 with
+  | .error failure, .error decisionFailure =>
+      failure.rejectedCandidates == 1 && 0 < failure.certAttempts &&
+        failure.certAttempts == decisionFailure.attempts &&
+        failure.rand == decisionFailure.rand
+  | _, _ => false)
 
 -- Sieve representation and a complete small-bound comparison with the
 -- independent trial-division decision route.