refactor(bz): migrate HexBerlekampZassenhausMathlib to the module system

HexBerlekampMathlib/Basic.lean

@@ -155,6 +155,7 @@ private theorem sum_ite_diagonal_eq_range_succ (f g : Hex.FpPoly p) (n : Nat) :
 The executable finite-field polynomial representation is ring-equivalent to
 Mathlib polynomials over `ZMod p`.
 -/
+@[expose]
 def fpPolyEquiv : Hex.FpPoly p ≃+* Polynomial (ZMod p) where
   toFun := fpPolyToPolynomial
   invFun := polynomialToFpPoly
@@ -209,6 +210,7 @@ def fpPolyEquiv : Hex.FpPoly p ≃+* Polynomial (ZMod p) where
     exact HexModArithMathlib.ZMod64.toZMod_add _ _
 
 /-- Interpret an executable `FpPoly p` as a Mathlib polynomial over `ZMod p`. -/
+@[expose]
 def toMathlibPolynomial (f : Hex.FpPoly p) : Polynomial (ZMod p) :=
   fpPolyEquiv f
 

HexBerlekampZassenhausMathlib.lean

@@ -4,19 +4,23 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexBerlekampZassenhausMathlib.Basic
-import HexBerlekampZassenhausMathlib.CertReify
-import HexBerlekampZassenhausMathlib.IrreducibleCert
-import HexBerlekampZassenhausMathlib.IrreducibleCertTest
-import HexBerlekampZassenhausMathlib.SignatureClasses
-import HexBerlekampZassenhausMathlib.Lattice
-import HexBerlekampZassenhausMathlib.CLDColumnBound
-import HexBerlekampZassenhausMathlib.Recovery
-import HexBerlekampZassenhausMathlib.PartitionRefinement
-import HexBerlekampZassenhausMathlib.UFDPartition
-import HexBerlekampZassenhausMathlib.IntReductionMod
-import HexBerlekampZassenhausMathlib.FactorSoundness
-import HexBerlekampZassenhausMathlib.LatticeTier
+module
+
+public import HexBerlekampZassenhausMathlib.Basic
+public import HexBerlekampZassenhausMathlib.CertReify
+public import HexBerlekampZassenhausMathlib.IrreducibleCert
+public import HexBerlekampZassenhausMathlib.IrreducibleCertTest
+public import HexBerlekampZassenhausMathlib.SignatureClasses
+public import HexBerlekampZassenhausMathlib.Lattice
+public import HexBerlekampZassenhausMathlib.CLDColumnBound
+public import HexBerlekampZassenhausMathlib.Recovery
+public import HexBerlekampZassenhausMathlib.PartitionRefinement
+public import HexBerlekampZassenhausMathlib.UFDPartition
+public import HexBerlekampZassenhausMathlib.IntReductionMod
+public import HexBerlekampZassenhausMathlib.FactorSoundness
+public import HexBerlekampZassenhausMathlib.LatticeTier
+
+public section
 
 /-!
 Root module for the Mathlib-side correspondence of the integer

HexBerlekampZassenhausMathlib/Basic.lean

@@ -4,15 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexBerlekampZassenhaus
-import HexBerlekampMathlib.Basic
-import HexBerlekampZassenhausMathlib.UFDPartition
-import HexHenselMathlib.Correctness
-import HexPolyZMathlib.Basic
-import HexPolyZMathlib.Mignotte
-import Mathlib.RingTheory.Coprime.Lemmas
-import Mathlib.RingTheory.Polynomial.UniqueFactorization
-import Mathlib.RingTheory.PrincipalIdealDomain
+module
+
+public import HexBerlekampZassenhaus
+public import HexBerlekampMathlib.Basic
+public import HexBerlekampZassenhausMathlib.UFDPartition
+public import HexHenselMathlib.Correctness
+public import HexPolyZMathlib.Basic
+public import HexPolyZMathlib.Mignotte
+public import Mathlib.RingTheory.Coprime.Lemmas
+public import Mathlib.RingTheory.Polynomial.UniqueFactorization
+public import Mathlib.RingTheory.PrincipalIdealDomain
+
+public section
+set_option backward.proofsInPublic true
+set_option backward.privateInPublic true
 
 /-!
 Mathlib-facing correctness surface for `HexBerlekampZassenhaus`.
@@ -158,6 +164,7 @@ Executable irreducibility predicate for transported integer polynomials.
 The checker delegates to the Mathlib-free `Hex.ZPoly` executable predicate
 after transporting the Mathlib polynomial into the project representation.
 -/
+@[expose]
 def irreducibleByFactorization (f : Polynomial ℤ) : Bool :=
   Hex.ZPoly.isIrreducible (HexPolyZMathlib.ofPolynomial f)
 
@@ -1300,6 +1307,7 @@ The monic modular image used for subset partition statements. This mirrors the
 executable prime-choice normalization: zero stays zero, and nonzero inputs are
 scaled by the inverse of their leading coefficient.
 -/
+@[expose]
 def monicModPImage {p : Nat} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) : Hex.FpPoly p :=
   if f.isZero then
     0
@@ -2055,6 +2063,7 @@ abbrev LiftedFactorSubset (d : Hex.LiftData) : Type :=
   Finset (LiftedFactorIndex d)
 
 /-- The lifted local factor at an executable `LiftData` index. -/
+@[expose]
 def liftedFactor (d : Hex.LiftData) (i : LiftedFactorIndex d) : Hex.ZPoly :=
   d.liftedFactors[i]
 
@@ -2063,6 +2072,7 @@ def liftedFactorProduct (d : Hex.LiftData) (S : LiftedFactorSubset d) : Hex.ZPol
   S.toList.foldl (fun acc i => acc * liftedFactor d i) 1
 
 /-- Transport a modular-factor index to the corresponding lifted-factor index. -/
+@[expose]
 def liftedIndexOfModPIndex
     (primeData : Hex.PrimeChoiceData) (d : Hex.LiftData)
     (hsize : d.liftedFactors.size = primeData.factorsModP.size)
@@ -2208,6 +2218,7 @@ leading-coefficient dilation has primitive part equal to the integer factor.
 The public predicate is proof-only; helper lemmas can unpack the underlying
 `RecoveredAtLift` witness when they need the monic-coordinate data.
 -/
+@[expose]
 def RepresentsIntegerFactorAtLift
     (core : Hex.ZPoly) (d : Hex.LiftData) (factor : Hex.ZPoly)
     (S : LiftedFactorSubset d) : Prop :=
@@ -3766,6 +3777,7 @@ The accompanying partition lemmas specialize to the full lifted-index universe
 `J = Finset.univ`; proper recursive rest partitions keep their remaining-index
 guard outside this support family.
 -/
+@[expose]
 def liftedTrueSupports (core : Hex.ZPoly) (d : Hex.LiftData) :
     Set (Set (LiftedFactorIndex d)) :=
   fun U =>
@@ -17335,6 +17347,7 @@ at the top.  See `progress/20260701T002411Z_issue-8413-smart-coverage.md`.
 The wrapper `Hex.scaledRecombinationSmart` passes `budget + smartFuelBound r`
 (its `(r+1)(2r+3)` term). Quadratic because the size loop's per-level overhead
 sums to `O(r²)` over the peel recursion. -/
+@[expose]
 def smartFuelBound (n : Nat) : Nat := (n + 1) * (2 * n + 3)
 
 /-- Fuel budget for the size/candidate loops at `n` remaining lifted factors;
@@ -19758,9 +19771,18 @@ theorem exists_factor_of_modPIndex
           @monicModPImage primeData.p primeData.bounds
               (@Hex.ZPoly.modP primeData.p primeData.bounds g) = 0 := by
         unfold monicModPImage
-        simp [hzero]
+        rw [if_pos hzero]
       rw [hmonic_zero]
-      exact dvd_zero _
+      have hz : HexBerlekampMathlib.toMathlibPolynomial
+          (0 : Hex.FpPoly primeData.p) = 0 := by
+        apply Polynomial.ext
+        intro n
+        rw [Polynomial.coeff_zero, HexBerlekampMathlib.coeff_toMathlibPolynomial,
+          Hex.DensePoly.coeff_eq_zero_of_size_le _
+            (show (0 : Hex.FpPoly primeData.p).size ≤ n by simp)]
+        exact HexModArithMathlib.ZMod64.toZMod_zero
+      rw [hz]
+      exact dvd_zero (f i)
     · have hnz :
           (@Hex.ZPoly.modP primeData.p primeData.bounds g).isZero = false := by
         cases h :

HexBerlekampZassenhausMathlib/CLDColumnBound.lean

@@ -4,14 +4,20 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexBerlekampZassenhaus
-import HexBerlekampZassenhausMathlib.Lattice
-import HexHenselMathlib.Correctness
-import HexPolyZMathlib.Mignotte
-import HexPolyZMathlib.RobinsonForm
-import Mathlib.Algebra.Polynomial.FieldDivision
-import Mathlib.Algebra.BigOperators.Ring.Multiset
-import Mathlib.Data.Nat.Choose.Bounds
+module
+
+public import HexBerlekampZassenhaus
+public import HexBerlekampZassenhausMathlib.Lattice
+public import HexHenselMathlib.Correctness
+public import HexPolyZMathlib.Mignotte
+public import HexPolyZMathlib.RobinsonForm
+public import Mathlib.Algebra.Polynomial.FieldDivision
+public import Mathlib.Algebra.BigOperators.Ring.Multiset
+public import Mathlib.Data.Nat.Choose.Bounds
+
+public section
+set_option backward.proofsInPublic true
+set_option backward.privateInPublic true
 
 /-!
 BHKS CLD-column coefficient bounds (van Hoeij `W ⊆ L'` analytics, #8519).

HexBerlekampZassenhausMathlib/CertReify.lean

@@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexBerlekampZassenhaus
-import Lean
+module
+
+public import HexBerlekampZassenhaus
+public import Lean
+
+public section
 
 /-!
 Elaboration-time reification of `Hex.ZPolyIrreducibilityCertificate` values as

HexBerlekampZassenhausMathlib/FactorSoundness.lean

@@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexBerlekampZassenhausMathlib.IntReductionMod
-import HexBerlekampZassenhausMathlib.LatticeTier
+module
+
+public import HexBerlekampZassenhausMathlib.IntReductionMod
+public import HexBerlekampZassenhausMathlib.LatticeTier
+
+public section
 
 /-!
 Public factorization soundness surface that needs the post-`IntReductionMod`

HexBerlekampZassenhausMathlib/IntReductionMod.lean

@@ -4,17 +4,23 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexBerlekampZassenhausMathlib.Basic
-import HexBerlekampMathlib.Basic
-import Mathlib.Data.ZMod.Basic
-import Mathlib.RingTheory.Polynomial.Content
-import Mathlib.Algebra.Polynomial.Degree.Lemmas
-import Mathlib.Algebra.Polynomial.Eval.Degree
-import Mathlib.Algebra.Polynomial.Eval.Irreducible
-import Mathlib.FieldTheory.Separable
-import Mathlib.FieldTheory.Perfect
-import Mathlib.RingTheory.Polynomial.Radical
-import Mathlib.RingTheory.Polynomial.GaussLemma
+module
+
+public import HexBerlekampZassenhausMathlib.Basic
+public import HexBerlekampMathlib.Basic
+public import Mathlib.Data.ZMod.Basic
+public import Mathlib.RingTheory.Polynomial.Content
+public import Mathlib.Algebra.Polynomial.Degree.Lemmas
+public import Mathlib.Algebra.Polynomial.Eval.Degree
+public import Mathlib.Algebra.Polynomial.Eval.Irreducible
+public import Mathlib.FieldTheory.Separable
+public import Mathlib.FieldTheory.Perfect
+public import Mathlib.RingTheory.Polynomial.Radical
+public import Mathlib.RingTheory.Polynomial.GaussLemma
+
+public section
+set_option backward.proofsInPublic true
+set_option backward.privateInPublic true
 
 /-!
 Reduction-mod-`p` irreducibility lemma for primitive integer polynomials, used

HexBerlekampZassenhausMathlib/IrreducibleCert.lean

@@ -4,8 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexBerlekampZassenhausMathlib.Basic
-import HexBerlekampZassenhausMathlib.CertReify
+module
+
+public meta import HexBerlekampZassenhausMathlib.CertReify
+public import HexBerlekampZassenhausMathlib.Basic
+public import HexBerlekampZassenhausMathlib.CertReify
+
+public section
+set_option backward.proofsInPublic true
+set_option backward.privateInPublic true
 
 /-!
 The `irreducible_cert` tactic: certifying irreducibility for integer
@@ -33,26 +40,26 @@ namespace HexBerlekampZassenhausMathlib.IrreducibleCert
 
 open Lean Meta
 
-private unsafe def evalZPolyUnsafe (e : Expr) :
+private meta unsafe def evalZPolyUnsafe (e : Expr) :
     MetaM (Except String Hex.ZPoly) :=
   try
     return .ok (← evalExpr Hex.ZPoly (mkConst ``Hex.ZPoly) e)
   catch ex =>
     return .error (← ex.toMessageData.toString)
 
 @[implemented_by evalZPolyUnsafe]
-private opaque evalZPolyCore (e : Expr) : MetaM (Except String Hex.ZPoly)
+private meta opaque evalZPolyCore (e : Expr) : MetaM (Except String Hex.ZPoly)
 
 /-- Evaluate a closed `Hex.ZPoly` expression to its runtime value at
 elaboration time (compiled/interpreted evaluation, not kernel reduction). -/
-def evalZPoly (e : Expr) : MetaM Hex.ZPoly := do
+meta def evalZPoly (e : Expr) : MetaM Hex.ZPoly := do
   match ← evalZPolyCore e with
   | .ok f => return f
   | .error msg =>
       throwError "irreducible_cert: failed to evaluate the polynomial\
           {indentExpr e}\n{msg}"
 
-private unsafe def evalCertificateUnsafe (e : Expr) :
+private meta unsafe def evalCertificateUnsafe (e : Expr) :
     MetaM (Except String Hex.ZPolyIrreducibilityCertificate) :=
   try
     return .ok (← evalExpr Hex.ZPolyIrreducibilityCertificate
@@ -61,12 +68,12 @@ private unsafe def evalCertificateUnsafe (e : Expr) :
     return .error (← ex.toMessageData.toString)
 
 @[implemented_by evalCertificateUnsafe]
-private opaque evalCertificateCore (e : Expr) :
+private meta opaque evalCertificateCore (e : Expr) :
     MetaM (Except String Hex.ZPolyIrreducibilityCertificate)
 
 /-- Evaluate a closed `Hex.ZPolyIrreducibilityCertificate` expression to its
 runtime value at elaboration time. Used by the reification round-trip tests. -/
-def evalCertificate (e : Expr) : MetaM Hex.ZPolyIrreducibilityCertificate := do
+meta def evalCertificate (e : Expr) : MetaM Hex.ZPolyIrreducibilityCertificate := do
   match ← evalCertificateCore e with
   | .ok cert => return cert
   | .error msg =>
@@ -77,7 +84,7 @@ def evalCertificate (e : Expr) : MetaM Hex.ZPolyIrreducibilityCertificate := do
 Match a goal of the form `Irreducible (HexPolyZMathlib.toPolynomial f)`
 (or the unfolded `HexPolyMathlib.toPolynomial` at `R = ℤ`) and return `f`.
 -/
-private def matchIrreducibleGoal (tgt : Expr) : MetaM (Option Expr) := do
+private meta def matchIrreducibleGoal (tgt : Expr) : MetaM (Option Expr) := do
   let tgt ← whnfR tgt
   let_expr Irreducible _M _inst arg := tgt | return none
   if arg.getAppFn.isConstOf ``HexPolyZMathlib.toPolynomial &&

HexBerlekampZassenhausMathlib/IrreducibleCertTest.lean

@@ -4,7 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexBerlekampZassenhausMathlib.IrreducibleCert
+module
+
+public meta import HexBerlekampZassenhausMathlib.IrreducibleCert
+public import HexBerlekampZassenhausMathlib.IrreducibleCert
+-- The `irreducible_cert` proofs attach `Eq.refl true` for each certificate
+-- check, so the kernel must reduce `checkIrreducibleCertLinear` (and its
+-- Berlekamp pow-chain replay) plus the `Array`/`DensePoly` `==` comparisons.
+-- Expose those executable checker bodies and the efficient `Array` DecidableEq.
+import all HexBerlekampZassenhaus.Basic
+import all HexBerlekamp.Irreducibility
+import all Init.Data.Array.DecidableEq
+
+public section
+set_option backward.proofsInPublic true
+set_option backward.privateInPublic true
 
 /-!
 End-to-end tests for certificate reification and the `irreducible_cert`
@@ -38,7 +52,7 @@ def cubicInert : Hex.ZPoly := Hex.DensePoly.ofCoeffs #[-1, -1, 0, 1]
 /-- Reify the generated certificate (and the polynomial itself), typecheck
 them, evaluate them back, and compare with the originals; also confirm the
 evaluated copy still passes the kernel checker's compiled form. -/
-private def roundTrips (f : Hex.ZPoly) : MetaM Bool := do
+private meta def roundTrips (f : Hex.ZPoly) : MetaM Bool := do
   match Hex.certifyIrreducible? f with
   | none => return false
   | some cert => do