feat(primality): add the norm_num extension and Nat.Prime tactic reach - #9487
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
Elab.lean adds primality n and the three tactic forms per the SPEC: compiled certificate search at elaboration time from the reproducible seed, defeq transparency and bit-budget checks, verdict and exhaustion diagnostics, an untrusted-search self-check with the same compiled checkPrime the kernel replays, and an emitted term applying prime_of_checkPrimeAt to the reified certificate with one Eq.refl true slot. In-module tests cover every syntax form across all three decision tiers and the failure messages. Progress: progress/20260822T044810Z_primality-tactic.md Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
…rion Cert3.lean proves pocklington3, the BLS m = 1 theorem, Mathlib-free: divisor_mod_one lifts the per-prime-divisor congruence to all divisors; the certificate equation abF + (a+b) = 2sF + r pins the composite split; parity (R odd, F even) forces the mod-F offset even, which r < 2F kills on one side and the size-bound cap 2s <= 2F + r (two_s_le) kills on the other; the discriminant identity r^2 = (a-b)^2 + 8s then contradicts each disjunct of the condition. not_square_of_sqrt_witness is the two-multiplication witness form of the integer-square test for the checker. Progress: progress/20260822T045935Z_primality-bls.md Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
checkPock3Arith gains the real Brillhart-Lehmer-Selfridge conditions with the stored square-root witness; pock_divisor_step is factored out and shared by both soundness cases; the pock3 case of checker soundness closes through pocklington3; certificate search routes to mkPock3 when the factored part misses the square root, with the wrapper's checkPrime validation deciding acceptance. Guards cover the 199/F=6 cube-root acceptance and one rejection per condition. The SPEC records the except-step-4 correction, the witness-based discriminant test, and Nat.sqrt's removal from the replay closure. Progress: progress/20260822T050441Z_primality-pock3.md Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
Scaffolds HexPrimalityMathlib and adds Prime.lean (prime_iff via prime_iff_forall_lt against Nat.prime_def_lt, plus Nat.Prime-flavoured transports of the checker, decision, Miller-Rabin, and next-prime theorems; no DecidablePred Nat.Prime instance, per SPEC) and Segment.lean (primeTable_spec, primesIn_spec, filter_prime_range, and the forall_prime_lt scaffold for segment statements). Progress: progress/20260822T050700Z_primality-companion.md Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
Elab.lean generalizes provePrime to provePrimeWith and defers root Nat.Prime goals from the bare tactic; the companion's NormNum.lean adds the certificate-backed norm_num extension (threshold-deferred positives via the reified certificate, negatives via a validated rho factor and deriveNotPrime), the Nat.Prime goal handler on the shared primality syntax kind, and the evalNatPrimeTrial alias supporting the documented per-file opt-in that puts the certificate extension ahead of Mathlib's trial division. NormNumTests.lean exercises both verdicts at 31 bits plus the alias fallback. Progress: progress/20260823T230607Z_primality-normnum.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
added 26 commits
August 24, 2026 13:09
# Conflicts: # .github/workflows/ci.yml
# Conflicts: # HexPrimality.lean # scripts/bench/proof_only_runtime_exemptions.json
# Conflicts: # scripts/bench/proof_only_runtime_exemptions.json
# Conflicts: # HexPrimality.lean
# Conflicts: # .github/workflows/ci.yml # scripts/bench/proof_only_runtime_exemptions.json
# Conflicts: # HexPrimalityMathlib.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 milestone 5 of HexPrimality/SPEC/hex-primality.md.
Elab.leangeneralizesprovePrimetoprovePrimeWith headand makes the bare tactic defer rootNat.Primegoal shapes, so the companion registers a handler on the sameprimalitysyntax kind that emitsnatPrime_of_checkPrimeAtover the same reified certificate —by primalitynow closes bothHex.Nat.PrimeandNat.Primegoals with a kernel replay of the checker alone.NormNum.leanadds the certificate-backednorm_numextension: numerals belownatPrimeCertThresholdare deferred to Mathlib's trial division; above it, positive verdicts emit the reified certificate and negative verdicts a dynamically validated rho factor through Mathlib'sderiveNotPrime, with hard-semiprime exhaustion failing silently rather than computing without bound. One real finding is documented prominently:norm_numconsults extensions in registration order, Mathlib's trial-division extension registers first and on large numerals succeeds at elaboration with minFac chains the kernel cannot check past ~25 bits, and extension erasure does not persist across imports — so certificate-backednorm_numis a per-file opt-in (attribute [-norm_num] Mathlib.Meta.NormNum.evalNatPrime), with the re-registeredevalNatPrimeTrialalias keeping small numerals working in opted-in files.NormNumTests.leanexercises the pattern: certificate and rho-witness verdicts at 31 bits, alias trial division below the threshold. The route with no caveat remainsby primality.Stacked on #9412.
🤖 Prepared with Claude Code