refactor(bz): migrate HexBerlekampZassenhausMathlib to the module system - #8600
Merged
Conversation
Migrate the Mathlib-side Berlekamp-Zassenhaus correspondence library (the 13 files under `HexBerlekampZassenhausMathlib/` plus the umbrella) onto the Lean 4 module system, the Phase-1b follow-up to #8597 and the prerequisite for the Phase-2 split of the 22k-line `Basic.lean`. Per file: `module`, `public import`, `public section`, and the `backward.{proofsInPublic,privateInPublic}` crutch where private decls are referenced in public. The bridge proves correctness by unfolding executable and Mathlib-side defs, so it needs a large `@[expose]` pass (89 defs, driven outward from each "not an exposed body" / "not unfolded because not exposed" error until green) spanning the executable `HexBerlekampZassenhaus`/`HexHensel` layers, the `HexBerlekampMathlib`/`HexPolyZMathlib` bridges, and the library's own defs. The `irreducible_cert` tactic and its tests need their elaboration-time helpers marked `meta` (`public meta import` for the reifier), and the certificate kernel replay reduces `checkIrreducibleCertLinear` and its Berlekamp pow-chain plus `Array`/`DensePoly` `==` through `import all` of the executable checker modules and `Init.Data.Array.DecidableEq`. Two proof-text repairs in the `monicModPImage`-zero branch adapt to module reduction (a `simp` that started leaving a spurious `SemigroupWithZero` metavariable, and a `dvd_zero` on `toMathlibPolynomial 0`); no theorem statements change. See progress/20260704T141029Z_bz-mathlib-module-migration-phase1b.md. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
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 migrates the Mathlib-side Berlekamp-Zassenhaus correspondence library (the 13 files under
HexBerlekampZassenhausMathlib/plus the umbrella) onto the Lean 4 module system, the Phase-1b follow-up to #8597 ("refactor(bz): migrate HexBerlekampZassenhaus to the module system") and the prerequisite for the Phase-2 split of the 22k-lineBasic.lean. Per file it prependsmodule, rewritesimport Xtopublic import X, appendspublic sectionplus thebackward.{proofsInPublic,privateInPublic}crutch where private decls are referenced in public, and leaves existingprivatedecls private.The bridge proves correctness by unfolding executable and Mathlib-side defs, so it needs a large
@[expose]pass (89 defs, driven outward from each "not an exposed body" / "not unfolded because not exposed" / "not an inductive datatype" error until green) spanning the executableHexBerlekampZassenhaus/HexHensellayers, theHexBerlekampMathlib/HexPolyZMathlibbridges, and the library's own defs.The
irreducible_certtactic and its tests need their elaboration-time helpers markedmeta(withpublic meta importfor the reifier), and the certificate kernel replay reducescheckIrreducibleCertLinearand its Berlekamp pow-chain plusArray/DensePoly==throughimport allof the executable checker modules andInit.Data.Array.DecidableEq(the recipe's kernel-reduction tool, mirroring the executable side).Two proof-text repairs in the
monicModPImage-zero branch adapt to module reduction (asimpthat started leaving a spuriousSemigroupWithZerometavariable, and advd_zeroontoMathlibPolynomial 0); no theorem statements change.Verified: full
lake buildgreen (4088 jobs, 0 sorries in the diff),HexBerlekampZassenhausMathlibgreen,HexConformancegreen, BZ bench/emit exes green,python scripts/check_dag.pyexit 0, and nosorry/axiom/native_decideadded.Closes #8598.
🤖 Prepared with Claude Code