refactor: decide primality instead of hand-writing it, and commit the example field - #9300
Merged
Conversation
added 2 commits
August 20, 2026 05:26
… example field Adds a Decidable instance for Hex.Nat.Prime, via a bounded restatement of the divisor condition, so a concrete prime is by decide. Nine hand-written divisor case splits across HexConway, HexBerlekamp, HexGF2Mathlib, and four manual chapters collapse to one line each. Commits GF(5^4) as HexGFqField/Example.lean: the modulus x^4 + 2, its Rabin certificate, the checked irreducibility proof, and the field. The manual's two worked examples cited a certificate they rebuilt inline, with an 8M-heartbeat and 131072-recursion bump in the chapter text; they now cite the committed result. Exposes checkIrreducibilityCertificateLinear and checkPowChainLinear. Without exposed bodies, decide gets stuck on the unreduced application from a module file, so the checker's own docstring promise that 'rabinTest f hmonic = true should be discharged by decide' was unreachable for exactly the callers it was written for. Documents the two table-regeneration commands in the HexConway chapter and links it downstream to hex-gfq and hex-gfq-field. Progress file: progress/20260820T120000Z_finite-field-completion.md
… the proof-only source changes CI reported 'pclmul did not compile on this host; skipping' and exited zero: the x86 wrapper reads the high half with _mm_extract_epi64, which is SSE4.1, so -mpclmul alone leaves it uninlinable. Adds -msse4.1, and removes the skip-on-failure branch that turned that into a pass. A check whose whole purpose is to run both compiled paths must not report success when one of them did not build. Records the two source changes this branch makes to measured factorization inputs as proof-only: new declarations on a Prop-valued predicate, and two @[expose] attributes, neither of which alters compiled code.
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 adds a
Decidableinstance forHex.Nat.Prime, through a bounded restatement of the divisor condition, so that a concrete prime isby decide. Nine hand-written divisor case splits acrossHexConway,HexBerlekamp,HexGF2Mathlib, and four manual chapters collapse to one line each.It commits
GF(5^4)asHexGFqField/Example.lean: the modulusx^4 + 2, its Rabin certificate, the checked irreducibility proof, and the field itself. Both manual worked examples previously rebuilt that certificate inline, carrying an 8M-heartbeat and 131072-recursion bump in the chapter text; they now cite the committed result instead.Exposing
checkIrreducibilityCertificateLinearandcheckPowChainLinearis what makes that possible. Without exposed bodiesdecidegets stuck on the unreduced application from amodulefile, so the checker's own docstring promise thatrabinTest f hmonic = true"should be discharged bydecide" was unreachable for precisely the callers it was written for.Finally, the
HexConwaychapter gains a section on the two table-regeneration commands and links tohex-gfqandhex-gfq-field.🤖 Prepared with Claude Code