refactor(bz): migrate HexBerlekampZassenhausMathlib to the module system

[kim-em]

Phase 1b of the Berlekamp-Zassenhaus module-system migration. Phase 1a (the executable HexBerlekampZassenhaus library) landed in #8597; this issue is the Mathlib bridge. Do this before the Phase 2 split (tracked separately) — the split of HexBerlekampZassenhausMathlib/Basic.lean requires the library to be on the module system first.

Scope

Migrate every file in HexBerlekampZassenhausMathlib/ plus the umbrella HexBerlekampZassenhausMathlib.lean onto the Lean 4 module system (module / public import X / public section), following the same recipe as #8597 and the earlier b33b904b (HexBerlekamp + HexBerlekampMathlib) migration.

Files: HexBerlekampZassenhausMathlib.lean (umbrella) and under HexBerlekampZassenhausMathlib/: Basic (22,707 lines), CertReify, IrreducibleCert, IrreducibleCertTest, SignatureClasses, Lattice, CLDColumnBound, Recovery, PartitionRefinement, UFDPartition, IntReductionMod, FactorSoundness, LatticeTier.

Why this is the harder half

• It is CI-gated. ci.yml builds the whole HexBerlekampZassenhausMathlib library (transitively HexBerlekampMathlib), so it is merge-gating and must stay green. See the hex-lean-mathlib-boundary skill.
• Expect a larger @[expose] / private-in-public pass than the executable side: the Mathlib layer proves correctness by unfolding executable defs, and it has ~140 private decls in Basic.lean alone.

Recipe (from #8597)

Per file: prepend module; rewrite import X -> public import X; append public section (module docstring + namespace + noncomputable section stay after it); keep existing private decls private. Then:

1. public meta import any module whose compiled code #guard/#eval/decide-at-elaboration evaluates through (mirror what HexBerlekampZassenhaus/Basic.lean needed).
2. set_option backward.proofsInPublic true / backward.privateInPublic true after public section for private-in-public references (the same crutch HexPoly/Euclid and the executable BZ use).
3. @[expose] the defs (executable and Mathlib-side) that exported rfl/simp/decide/unfold/change proofs reduce through. Build and add @[expose] outward from the first real error until green.
4. Leaked-instance audit: de-privatise (or reach via import all) any private instance the bridge relies on through legacy resolution (Phase 1a hit GcdLaws Rat).
5. import all Init.Data.Array.DecidableEq where decide/rfl over Array/DensePoly equality must reduce (the Array.instDecidableEqImpl bug, upstream fix fix: expose Array equality for kernel reduction leanprover/lean4#14270). Note DensePoly.leadingCoeff is already the getD (size-1) form after refactor(bz): migrate HexBerlekampZassenhaus to the module system #8597, so the Array.back? workaround is already in place.

Two leadingCoeff = 0 proofs in HexBerlekampZassenhausMathlib/Basic.lean were already fixed in #8597 (they broke on the leadingCoeff reimplementation); nothing else in the file was touched.

Constraints

• No native_decide, no axiom, no sorry (SPEC).
• scripts/check_dag.py must pass (umbrella public imports every module; no change to check_dag.py needed).
• Do not split any file in this issue — that is Phase 2. This is a pure migration; no declaration moves or renames.

Verify

Full lake build green (ending at 0 sorries), python scripts/check_dag.py, and the HexConformance target. git diff should show only module-system boilerplate + @[expose] + a few proof-text repairs, no theorem-statement changes.

🤖 Prepared with Claude Code