feat(primality): add certificate search and the bounded decision API - #9402
Merged
Conversation
…visor lemmas powModNat gains the p = 0 guard so it agrees with powMod at every input, its recursion (powModNatGo, bitLength) is @[expose]d, its correctness theorem is exported, and an unconditional @[csimp] names powModNat the kernel-facing specification with powMod the runtime twin. instDecidablePrime re-routes decide through isPrimeTrial, exists_trial_divisor is exported, and exists_prime_dvd plus exists_prime_le_sqrt are the composite-witness lemmas the hex-primality Pocklington argument finishes with. SPEC amendments record the landed state (hex-arith SPEC modular-exponentiation and primality sections; hex-primality SPEC stale claims corrected). Progress: progress/20260822T034253Z_primality-m0.md Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
… at 10^4 Adds the HexPrimality library (deps HexArith, HexBasic) with its umbrella, libraries.yml entry, CI lib target, and the SPEC co-located at HexPrimality/SPEC/hex-primality.md. Table.lean commits the 1229-entry primeTable below primeTableBound = 10000 with sortedness, binary-search membership (isTablePrime_iff), soundness via one kernel-replayed isPrimeTrial sweep, completeness via five balanced kernel-replayed coverOk chunks, and primesIn with its membership theorem. Statements are sieve-agnostic so the planned kernel-reducible sieve swaps proof internals only. Progress: progress/20260822T040440Z_primality-table.md Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
Order.lean defines orderOf as a bounded least-search with junk value 0 off the coprime domain and proves the SPEC's order stack Mathlib-free: coprimality from a unit power, coprime cancellation, multiplicative Fermat, order positivity via pigeonhole through the ListShim, order divisibility both ways, orderOf_dvd_pred, prime-power extraction into the order, and the two square roots of 1 modulo a prime. Progress: progress/20260822T041921Z_primality-order.md Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
…tion MillerRabin.lean adds oddSplit with its spec, the squaring loop, and millerRabin with the SPEC's exact branch table, plus defaultBases and isProbablePrime. Soundness is the contrapositive millerRabin_eq_true_of_prime by forward induction along the loop with sq_roots_of_one; not_prime_of_millerRabin_false is the public theorem, and no completeness is claimed. Guards cover Carmichael numbers, strong pseudoprimes, and agreement with isPrimeTrial below 512. Progress: progress/20260822T042306Z_primality-millerrabin.md Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
Implements the hex-finite-field SPEC's Randomness section at its specified site in hex-basic: Rand with next, RandError carrying the advanced state on exhaustion, Rand.nat by rejection sampling that rejects the incomplete top interval, Rand.ofSeed, and the range theorem Rand.nat_lt. Known-answer guards pin the canonical splitmix64 seed-0 vector and deterministic replay. Progress: progress/20260822T042502Z_hexbasic-rand.md Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
…e checker Cert.lean defines PrimeCert (with the pock3 constructor carrying the integer-square-root witness the SPEC amendment records, its arithmetic stubbed false until milestone 4), the structurally recursive checkPrime/checkChildren pair with all workers @[expose]d against the kernel-facing powModNat, and checker soundness prime_of_checkPrime by strong induction on the subject value, through the pocklington core theorem, the fused coprime-prime-power combination, and the gcd-to-noncongruence transport. CheckedPrimeCert and the single-Bool-slot prime_of_checkPrimeAt serve the coming search and tactic layers. Guards cover accepted multi-level certificates and one rejected certificate of each kind. Progress: progress/20260822T043327Z_primality-cert.md Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
Search.lean adds RhoStop/RhoFailure with the resumable-failure convention, rhoFactor? as Brent cycle search with restart draws from Hex.Rand and dynamic validation at every success exit (making rhoFactor?_spec a fuel induction over guards), and the internal partialFactor: table trial division, then a rho worklist whose every path preserves the product exactly, giving the unconditional partialFactor_prod invariant. Progress: progress/20260822T044003Z_primality-rho.md Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
Search.lean gains the resumable failure types, the mutual fuel-and-worklist certificate search primeCertGo/assembleGo (runtime only, so well-founded recursion is fine), the indexed primeCert? whose runtime dependent checks build CheckedPrimeCert with zero proof plumbing, the verdict theorem primeCert?_composite by path analysis, isPrime? across the table/trial/certificate tiers with its exactness spec, the total isPrime with unconditional isPrime_iff, and nextPrime? with its leastness spec. Progress: progress/20260822T044458Z_primality-decide.md Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
The stack changes factor-sweep-relevant sources with no effect on the factorization service: the powModNat kernel-facing amendments and the Decidable (Prime p) reroute in hex-arith, the primality conformance emitters, the hotPathCandidates proof-carrying view with pinned values, and per-milestone lakefile registrations. Each transition gets an exact blob-pair exemption with its reason, and the file is unioned with main's current entries so the stack also inherits the HexBasic/Rand attestation that merged separately. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
# Conflicts: # scripts/bench/proof_only_runtime_exemptions.json
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
# Conflicts: # scripts/bench/proof_only_runtime_exemptions.json
# Conflicts: # .github/workflows/ci.yml # SPEC/future-work.md
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
rhoInnerFuel scaled as 16 * (n^(1/4) + 2) with no ceiling, so one Brent restart at 256+ bits had an effectively unbounded budget and a search whose smallest factor was out of reach hung inside the first restart instead of returning a clean exhausted. Capping at 2^22 binds only past n ~ 2^72 and still covers factors to about 2^44, beyond rho's documented ~10^12 remit; a semiprime with two ~2^35 factors still splits in 182 ms while one with two ~2^60 factors now exhausts cleanly at seconds per restart. The spec proofs are fuel-agnostic and unchanged, and the emitted conformance fixtures are byte-identical. Progress: progress/20260824T004117Z_primality-rho-cap.md Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9 (cherry picked from commit 7fb9f77)
Codex review of the decision core noted the counter reads as a global total; it counts only the failing search's restarts. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
Codex review of the decision core noted the counters read as global totals; each counts only its own failing subsearch, and the next-prime counter excludes the unresolved candidate. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
Tail-appended exemption entries conflict textually with every concurrent append on main; placing the stack's entries after the first entry keeps future main-side appends automatically mergeable. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
# Conflicts: # .github/workflows/ci.yml # scripts/bench/proof_only_runtime_exemptions.json
added 15 commits
August 24, 2026 12:19
# Conflicts: # HexArith/SPEC/hex-arith.md # scripts/bench/proof_only_runtime_exemptions.json
# Conflicts: # HexPrimality.lean
# Conflicts: # HexPrimality/Search.lean
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR completes the search half of milestone 3 in HexPrimality/SPEC/hex-primality.md.
primeCertGo/assembleGoare a mutual recursion on(fuel, worklist length)— runtime dispatch that appears in no proof term, so well-founded recursion is fine here — with verdict tiers first (size, table completeness, a Miller-Rabin base scan) and thenpartialFactor (n - 1), one certified child and one searched witness per claimed prime-power entry. A child-certification failure is reported as exhaustion, never as compositeness of the parent: a composite child only means the untrusted factorization guessed wrong.primeCert?builds the indexedCheckedPrimeCertthrough runtime dependent checks (zero proof plumbing), so a certificate for one number can never answer a request about another.primeCert?_compositeis proved by path analysis: the only.compositeexits are the three justified verdicts, andassembleGo_error_stopshows search failures cannot masquerade as verdicts. On top sitisPrime?(table belowprimeTableBound, exact trial below a placeholder threshold the bench will measure, then certificate search) withisPrime?_spec, the totalisPrimewhose trial fallback makesisPrime_iffunconditional, andnextPrime?with the leastness invariant carried through the scan.Guards cover all three decision tiers;
2^31 - 1exercises the certificate tier deterministically since itsn - 1factors entirely over the committed table.Stacked on #9401.
🤖 Prepared with Claude Code