feat(primality): add conformance fixtures and the PARI oracle - #9488
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
Adds the isprime/certcheck/segment fixture kinds (emitters in the shared Emit library, validation with a recursive certificate schema in common.py), the deterministic HexPrimality emit driver covering the SPEC's full case list including hand-built rejected certificates and the migrated hot-path window, the Conformance module per the testing contract, the primality_pari.py oracle (PARI verdicts and segments, python-flint second opinion, independent Python replay of the checker), the ORACLES tuple, lakefile and CI registrations, and the committed 96-record snapshot, locally cross-validated against a pure Python stand-in. Progress: progress/20260823T231919Z_primality-conformance.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
# Conflicts: # .github/workflows/ci.yml # scripts/bench/proof_only_runtime_exemptions.json
Codex review noted n.log2 alone admits an input one bit past the advertised ceiling; a positive numeral has n.log2 + 1 bits. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
Codex review noted a valid but non-literal goal like Nat.Prime (2 + 2) fell through both handlers to a generic unexpected-syntax error; once the companion handler owns a Nat.Prime target it now emits the same not-a-numeral diagnostic as the Mathlib-free handler, with a guarded regression test. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
The PARI oracle's certificate replay now mirrors boundedPowMul, multiplying one step at a time and aborting past n - 1 instead of constructing the full power, and the fixture validator requires every serialized Nat field to be nonnegative. The certcheck fixtures gain one rejection per checker clause that had no coverage: subjects below two, even subjects, duplicate subjects, the bounded-product abort, and the cube-root arm's even-cofactor, decomposition, r-range, size-bound, and second strict witness-window conditions, mirrored as checker #guards whose builds verify each construction rejects. The hot-path segment fixture moves out: it imported HexBerlekampZassenhaus from hex-primality's conformance driver, an inverted dependency that cannot publish with the split repo (it belongs beside BZ's own conformance when the hot-path migration lands). The Carmichael comment now says Fermat tests pass on coprime bases. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
# Conflicts: # .github/workflows/ci.yml
# Conflicts: # Hex/Conformance/Emit.lean # lakefile.lean # scripts/oracle/common.py
# Conflicts: # .github/workflows/ci.yml # lakefile.lean # scripts/bench/proof_only_runtime_exemptions.json
… ones An earlier merge resolution rebuilt Hex/Conformance/Emit.lean from a pre-truncated-series snapshot, silently dropping emitSeriesFixture and seriesValue and breaking HexTruncatedSeries.EmitFixtures in CI. The file is now main's current version with the primality emitters and boolValue inserted beside the modular-arithmetic block; both fixture executables build and their committed snapshots replay byte-identical. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0133rJ7x9mYiiXpJceCnc1A9
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 lands the hex-primality conformance surface per HexPrimality/SPEC/hex-primality.md §Conformance and SPEC/testing.md's five-step recipe. Three fixture kinds join the shared schema:
isprime,certcheck(the certificate rides as a raw JSON object; the serializer lives in the emitting driver because hex-test-kit cannot depend on HexPrimality), andsegment, with emitters inHex/Conformance/Emit.leanand validation — including a recursive certificate-shape validator — inscripts/oracle/common.py.The deterministic emit driver covers the SPEC's required cases: the 0-4 edges, prime squares and near-square-root semiprimes, all six Carmichael numbers, the four base-specific strong pseudoprimes,
2^k + 1, table/trial/certificate-tier verdicts (2^31 - 1and its composite neighbour), one accepted certificate per node kind including the cube-root arm, one hand-built rejected certificate per checker condition (no oracle produces negatives), segments including one straddlingprimeTableBound, and the migratedhotPathCandidateswindow pinning the view's contents and order.primality_pari.pyrecomputes verdicts and segments with PARI, takes python-flint as a second opinion where available, and replays certificates through an independent Python reimplementation whose small-table leaf uses the table's proven semantics. One tuple joinsORACLES; no new CI jobs. The committed 96-record snapshot is schema-validated and every result was cross-checked locally against a pure-Python stand-in (48/48), with emission verified byte-identical across runs; CI's cypari2 run is the authoritative check.Stacked on #9487.
🤖 Prepared with Claude Code