From 8ec6dadb8b09bfe892c3b6e6be9480a7ba485857 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 4 Jul 2026 14:11:08 +0000
Subject: [PATCH] refactor(bz): migrate HexBerlekampZassenhausMathlib to the
 module system

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>
---
 HexBerlekampMathlib/Basic.lean                |  2 +
 HexBerlekampZassenhaus/Basic.lean             | 60 +++++++++++++++++++
 HexBerlekampZassenhausMathlib.lean            | 30 ++++++----
 HexBerlekampZassenhausMathlib/Basic.lean      | 44 ++++++++++----
 .../CLDColumnBound.lean                       | 22 ++++---
 HexBerlekampZassenhausMathlib/CertReify.lean  |  8 ++-
 .../FactorSoundness.lean                      |  8 ++-
 .../IntReductionMod.lean                      | 28 +++++----
 .../IrreducibleCert.lean                      | 25 +++++---
 .../IrreducibleCertTest.lean                  | 18 +++++-
 HexBerlekampZassenhausMathlib/Lattice.lean    | 26 +++++++-
 .../LatticeTier.lean                          | 18 ++++--
 .../PartitionRefinement.lean                  | 10 +++-
 HexBerlekampZassenhausMathlib/Recovery.lean   | 10 +++-
 .../SignatureClasses.lean                     | 14 ++++-
 .../UFDPartition.lean                         | 18 ++++--
 HexHensel/Basic.lean                          |  1 +
 HexHensel/Multifactor.lean                    |  1 +
 HexHensel/QuadraticMultifactor.lean           |  1 +
 HexPolyZMathlib/Mignotte.lean                 |  1 +
 ...29Z_bz-mathlib-module-migration-phase1b.md | 52 ++++++++++++++++
 21 files changed, 317 insertions(+), 80 deletions(-)
 create mode 100644 progress/20260704T141029Z_bz-mathlib-module-migration-phase1b.md

diff --git a/HexBerlekampMathlib/Basic.lean b/HexBerlekampMathlib/Basic.lean
index a01527093..84eb9740b 100644
--- a/HexBerlekampMathlib/Basic.lean
+++ b/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
 
diff --git a/HexBerlekampZassenhaus/Basic.lean b/HexBerlekampZassenhaus/Basic.lean
index 2e964d547..77bb3a035 100644
--- a/HexBerlekampZassenhaus/Basic.lean
+++ b/HexBerlekampZassenhaus/Basic.lean
@@ -73,12 +73,14 @@ def extractXPower (f : ZPoly) : XPowerData :=
   { power := split.1, core := DensePoly.ofCoeffs split.2.toArray }
 
 /-- The integer leading coefficient reduced to the candidate prime field. -/
+@[expose]
 def leadingCoeffModP (f : ZPoly) (p : Nat) [ZMod64.Bounds p] : ZMod64 p :=
   ZMod64.ofNat p (intModNat (DensePoly.leadingCoeff f) p)
 
 end ZPoly
 
 /-- The candidate prime does not divide the integer leading coefficient. -/
+@[expose]
 def leadingCoeffAdmissible (f : ZPoly) (p : Nat) [ZMod64.Bounds p] : Prop :=
   ZPoly.leadingCoeffModP f p ≠ 0
 
@@ -1858,6 +1860,7 @@ def degreeSum (d : PrimeFactorData) : Nat :=
   d.factorDegrees.toList.foldl (fun acc n => acc + n) 0
 
 /-- Ordered product of the recorded modular factors for one prime. -/
+@[expose]
 def factorProduct (d : PrimeFactorData) : @FpPoly d.p d.bounds :=
   letI := d.bounds
   d.factorPolys.foldl (· * ·) 1
@@ -1866,6 +1869,7 @@ def factorProduct (d : PrimeFactorData) : @FpPoly d.p d.bounds :=
 def containsDegree (d : PrimeFactorData) (n : Nat) : Bool :=
   d.factorDegrees.toList.any fun degree => degree == n
 
+@[expose]
 def hasSubsetDegreeAux : List Nat → Nat → Bool
   | [], target => target == 0
   | degree :: degrees, target =>
@@ -1875,6 +1879,7 @@ def hasSubsetDegreeAux : List Nat → Nat → Bool
 /--
 Does some subset of this prime block's modular factor degrees sum to `target`?
 -/
+@[expose]
 def hasSubsetDegree (d : PrimeFactorData) (target : Nat) : Bool :=
   hasSubsetDegreeAux d.factorDegrees.toList target
 
@@ -1882,6 +1887,7 @@ def hasSubsetDegree (d : PrimeFactorData) (target : Nat) : Bool :=
 Check one nested finite-field irreducibility certificate against its degree slot
 and the concrete modular factor occupying that slot.
 -/
+@[expose]
 def checkCertAtFactor
     (d : PrimeFactorData) (degree : Nat) (factor : @FpPoly d.p d.bounds)
     (cert : Berlekamp.IrreducibilityCertificate) : Bool :=
@@ -1899,6 +1905,7 @@ def checkCertAtFactor
 Check that nested certificates match the enclosing prime, degree array, and
 concrete modular factor array.
 -/
+@[expose]
 def checkFactorCerts (d : PrimeFactorData) : Bool :=
   d.factorDegrees.size == d.factorCerts.size &&
     d.factorDegrees.size == d.factorPolys.size &&
@@ -1906,6 +1913,7 @@ def checkFactorCerts (d : PrimeFactorData) : Bool :=
       checkCertAtFactor d pair.1 pair.2.1 pair.2.2
 
 /-- Check one prime block against the integer polynomial being certified. -/
+@[expose]
 def checkForPolynomial (f : ZPoly) (d : PrimeFactorData) : Bool :=
   letI := d.bounds
   isGoodPrime f d.p &&
@@ -1919,10 +1927,12 @@ end PrimeFactorData
 namespace ZPolyIrreducibilityCertificate
 
 /-- Nontrivial integer factor degrees that must be ruled out for `f`. -/
+@[expose]
 def candidateFactorDegrees (f : ZPoly) : List Nat :=
   (List.range ((f.degree?.getD 0) / 2)).map fun i => i + 1
 
 /-- Look up a per-prime block by the index stored in an obstruction. -/
+@[expose]
 def primeDataAt? (cert : ZPolyIrreducibilityCertificate) (idx : Nat) :
     Option PrimeFactorData :=
   match cert.perPrime.toList.drop idx with
@@ -1940,6 +1950,7 @@ The target must be one of the nontrivial candidate degrees for `f`, and the
 referenced prime block must have no subset of modular factor degrees summing to
 that target.
 -/
+@[expose]
 def checkForCertificate
     (f : ZPoly) (cert : ZPolyIrreducibilityCertificate)
     (obs : DegreeObstruction) : Bool :=
@@ -1953,6 +1964,7 @@ end DegreeObstruction
 namespace ZPolyIrreducibilityCertificate
 
 /-- Does the obstruction array contain a valid obstruction for `targetDegree`? -/
+@[expose]
 def hasObstructionFor (f : ZPoly)
     (cert : ZPolyIrreducibilityCertificate) (targetDegree : Nat) : Bool :=
   cert.degreeObstructions.toList.any fun obs =>
@@ -2599,6 +2611,7 @@ tie-breaking is preserved. If the prefix exhausts without selecting any prime,
 the search folds over the fixed extended prime list through `499`, covering
 every odd prime in the SPEC hot-path interval `[3, 500]`.
 -/
+@[expose]
 def choosePrimeData? (f : ZPoly) : Option PrimeChoiceData :=
   match smallPrimeCandidates.foldl (choosePrimeDataScoreStep f) none with
   | some score => some score.data
@@ -2802,6 +2815,7 @@ instance required by `Berlekamp.berlekampFactor` is constructed explicitly
 from `hprime`, so callers can match it against any field instance built from
 the same prime witness via proof irrelevance of `ZMod64.PrimeModulus`.
 -/
+@[expose]
 def factorsModPBerlekampForm
     (f : ZPoly) (data : PrimeChoiceData) : Prop :=
   letI := data.bounds
@@ -3093,6 +3107,7 @@ def bhksBound (f : ZPoly) : Nat :=
   1 + n * 4 ^ (n * n) * (sumSquared + 1) ^ n * (Nat.log2 (sumSquared + 1)) ^ n
 
 /-- Integer coefficient bound `B_j` used by the BHKS all-coefficients CLD lattice. -/
+@[expose]
 def bhksCoeffBound (f : ZPoly) (j : Nat) : Nat :=
   let n := f.degree?.getD 0
   Nat.choose (n - 1) j * n * ZPoly.coeffL2NormBound f
@@ -3112,6 +3127,7 @@ For `1 < p`, `ceilLogP p target` searches for the least visible exponent
 whose `p`-power is at least `target`. The degenerate `p ≤ 1` case returns
 zero because the BHKS fast path is only used with admissible primes.
 -/
+@[expose]
 def ceilLogP (p target : Nat) : Nat :=
   if p ≤ 1 then
     0
@@ -3119,6 +3135,7 @@ def ceilLogP (p target : Nat) : Nat :=
     ceilLogPAux p target (target + 1) 0 1
 
 /-- Per-coordinate BHKS precision threshold `ell_j := ceil_log_p (2 * B_j + 1)`. -/
+@[expose]
 def bhksCoeffCutThreshold (p : Nat) (f : ZPoly) (j : Nat) : Nat :=
   ceilLogP p (2 * bhksCoeffBound f j + 1)
 
@@ -3131,6 +3148,7 @@ are different — `B` is a magnitude on integer coefficients, `a` is the
 small exponent on the Hensel modulus `p^a` — and must not be conflated.
 See SPEC/Libraries/hex-berlekamp-zassenhaus.md §"Slow path".
 -/
+@[expose]
 def precisionForCoeffBound (B p : Nat) : Nat :=
   ceilLogP p (2 * B + 1)
 
@@ -3270,6 +3288,7 @@ theorem precisionForCoeffBound_spec {p : Nat} (hp : 2 ≤ p) (B : Nat) :
 /-- Enumerate every way to partition a list of polynomials into a `(selected,
 unselected)` pair while preserving the original order in each component.  Used
 by the exhaustive recombination search to drive the slow path. -/
+@[expose]
 def subsetSplits : List ZPoly → List (List ZPoly × List ZPoly)
   | [] => [([], [])]
   | factor :: factors =>
@@ -3282,6 +3301,7 @@ into the `selected` component.  This is what the recombination search actually
 iterates over, since the head of the remaining local factors must end up in
 some recovered factor and tracking that explicitly avoids enumerating the same
 subset twice through different traversal orders. -/
+@[expose]
 def subsetSplitsWithFirst : List ZPoly → List (List ZPoly × List ZPoly)
   | [] => []
   | factor :: factors =>
@@ -3579,6 +3599,7 @@ The repeated-part expansion fully consumed the normalization residual, so
 `reassemblePolynomialFactors` uses its expanded branch rather than the
 non-decomposed repeated-part fallback.
 -/
+@[expose]
 def reassemblyExpansionComplete
     (d : FactorNormalizationData) (coreFactors : Array ZPoly) : Prop :=
   (expandRepeatedPartFactorArray d.repeatedPart coreFactors).2 = 1
@@ -4806,6 +4827,7 @@ def exhaustiveIntegerTrialCoreFactorsWithBound
   else
     (split.1 ++ peel.1).push peel.2
 
+@[expose]
 def centeredModNat (z : Int) (m : Nat) : Int :=
   if m = 0 then
     z
@@ -4875,6 +4897,7 @@ theorem centeredModNat_emod_eq_of_natAbs_le
       omega
 
 /-- Centred residue modulo `p^b`, the `mod^±` operation in the BHKS cut. -/
+@[expose]
 def centeredResiduePow (p b : Nat) (x : Int) : Int :=
   centeredModNat x (p ^ b)
 
@@ -4907,6 +4930,7 @@ Exposed (rather than private) so the BHKS bridge layer can state the
 congruence linking the executable quotient to the exact integer CLD
 coefficient.
 -/
+@[expose]
 def cldQuotientMod (f g : ZPoly) (p a : Nat) : ZPoly :=
   let numerator := ZPoly.reduceModPow (f * DensePoly.derivative g) p a
   let quotient := (DensePoly.divMod numerator g).1
@@ -5113,6 +5137,7 @@ theorem cldQuotientMod_divMod_reconstruction (f g : ZPoly) (p a : Nat)
   ZPoly.divMod_reconstruction_of_monic _ g hg
 
 /-- Per-coordinate BHKS cut thresholds for the all-coefficients CLD lattice. -/
+@[expose]
 def bhksCutThresholds (f : ZPoly) (p : Nat) : Array Nat :=
   let n := f.degree?.getD 0
   (List.range n).map (fun j => bhksCoeffCutThreshold p f j) |>.toArray
@@ -5160,6 +5185,7 @@ structure BhksProjectedRows where
   reducedRowCount : Nat
   projectedRows : Array (Array Int)
 
+@[expose]
 def bhksLatticeEntry
     (r n p a : Nat) (thresholds : Array Nat) (cldRows : Array (Array Int))
     (i j : Fin (r + n)) : Int :=
@@ -5184,6 +5210,7 @@ Build the BHKS all-coefficients CLD row-basis matrix
 The diagonal exponent uses natural subtraction; callers that need the exact
 BHKS hypotheses should lift to a precision `a` satisfying every `l_j ≤ a`.
 -/
+@[expose]
 def bhksLatticeBasis (f : ZPoly) (p a : Nat) (liftedFactors : Array ZPoly) :
     BhksLatticeBasis :=
   let r := liftedFactors.size
@@ -5268,9 +5295,11 @@ theorem bhksLatticeEntry_bottomRight_diag_pos
   exact Int.ofNat_lt.mpr hpos
 
 /-- Four times the squared BHKS cut radius, `4 * (r + n * (r / 2)^2)`. -/
+@[expose]
 def bhksCutRadiusSq4 (L : BhksLatticeBasis) : Nat :=
   4 * L.factorCount + L.coeffWidth * L.factorCount * L.factorCount
 
+@[expose]
 def bhksWithinGramSchmidtCut (L : BhksLatticeBasis)
     (dets : Vector Nat (L.factorCount + L.coeffWidth + 1))
     (i : Fin (L.factorCount + L.coeffWidth)) : Bool :=
@@ -5282,6 +5311,7 @@ def bhksWithinGramSchmidtCut (L : BhksLatticeBasis)
   else
     4 * ((d1 : Rat) / (d0 : Rat)) ≤ (bhksCutRadiusSq4 L : Rat)
 
+@[expose]
 def bhksProjectIndicator (r n : Nat) (v : Vector Int (r + n)) : Array Int :=
   (List.range r).map
     (fun j =>
@@ -5334,6 +5364,7 @@ the fold runs in increasing index order, the accumulator ends at
 contiguous prefix `b_0 … b_t` in original order — including earlier rows whose
 own Gram-Schmidt norm exceeds the radius.
 -/
+@[expose]
 def bhksCutPrefixCount
     (L : BhksLatticeBasis)
     (reduced : Matrix Int (L.factorCount + L.coeffWidth)
@@ -5345,6 +5376,7 @@ def bhksCutPrefixCount
       if bhksWithinGramSchmidtCut L dets i then i.val + 1 else acc)
     0
 
+@[expose]
 def bhksCutProjectReducedRows
     (L : BhksLatticeBasis)
     (reduced : Matrix Int (L.factorCount + L.coeffWidth)
@@ -5396,6 +5428,7 @@ structure BhksProjectedRowsTrace (L : BhksLatticeBasis) where
   projectedRetainedRows : Array (Array Int)
   projectedRows : Array (Array Int)
 
+@[expose]
 def bhksProjectedRowsTrace (L : BhksLatticeBasis)
     (hrows : 1 ≤ L.factorCount + L.coeffWidth) : BhksProjectedRowsTrace L :=
   let reducedRows :=
@@ -5425,6 +5458,7 @@ integer leading Gram determinant vector as `d_{i+1}/d_i`.
 The result is the executable `L'` row data consumed by the later RREF /
 equivalence-class recovery stage.
 -/
+@[expose]
 def bhksProjectedRows (L : BhksLatticeBasis)
     (hrows : 1 ≤ L.factorCount + L.coeffWidth) : BhksProjectedRows :=
   let reducedRows :=
@@ -5562,6 +5596,7 @@ sized `n × r`, with `n := L.projectedRows.size` and `r := L.factorCount`.
 The matrix is the input to BHKS Lemma 3.3 RREF-based equivalence-class
 identification.
 -/
+@[expose]
 def bhksProjectedRowsAsRatMatrix
     (rows : Array (Array Int)) (n r : Nat) : Matrix Rat n r :=
   Matrix.ofFn fun i j =>
@@ -5571,6 +5606,7 @@ private def bhksColumnSignature
     (echelonRows : Array (Array Rat)) (j : Nat) : Array Rat :=
   echelonRows.map (·.getD j 0)
 
+@[expose]
 def bhksInsertSignatureClass
     (sig : Array Rat) (j : Nat) :
     List (Array Rat × List Nat) → List (Array Rat × List Nat)
@@ -5594,6 +5630,7 @@ Algorithm 8). Each equivalence class produces one compact `0/1` indicator
 of length `r`. Classes are emitted in the order they are first observed by
 ascending column index.
 -/
+@[expose]
 def bhksEquivalenceClassIndicators (L : BhksProjectedRows) : Array (Array Int) :=
   let n := L.projectedRows.size
   let r := L.factorCount
@@ -5637,6 +5674,7 @@ private def bhksNoProgressProjectedRows : BhksProjectedRows :=
 #guard bhksEquivalenceClassIndicators bhksNoProgressProjectedRows =
   #[#[1, 0, 0], #[0, 1, 0], #[0, 0, 1]]
 
+@[expose]
 def liftModulus (d : LiftData) : Nat :=
   d.p ^ d.k
 
@@ -5682,6 +5720,7 @@ theorem centeredLiftPoly_eq_of_reduceModPow_eq
 flipping sign so the leading coefficient is non-negative.  Used by
 `bhksIndicatorCandidate?` to produce a canonical witness from the centred
 lift of a scaled lifted-factor product. -/
+@[expose]
 def normalizeCandidateFactor (candidate : ZPoly) : ZPoly :=
   let primitive := ZPoly.primitivePart candidate
   if DensePoly.leadingCoeff primitive < 0 then
@@ -7943,6 +7982,7 @@ def recombinationSearch (f : ZPoly) (localFactors : List ZPoly) : Option (List Z
 forced into the candidate, the centred-lift result is normalised and checked
 against `shouldRecordPolynomialFactor`, and a successful `exactQuotient?`
 divides the search down to the remaining local factors and quotient. -/
+@[expose]
 def recombinationSearchModAux
     (target : ZPoly) (modulus : Nat) (localFactors : List ZPoly) :
     Nat → Option (List ZPoly)
@@ -7993,6 +8033,7 @@ collapse recovers the original unscaled `recombinationSearchModAux` candidate
 shape; for primitive non-monic cores this yields the primitive integer factor of
 `core` whose `RepresentsIntegerFactorAtLift` certificate drives the recursive
 coverage chain. -/
+@[expose]
 def scaledRecombinationSearchModAux
     (coreLc : Int) (target : ZPoly) (modulus : Nat) (localFactors : List ZPoly) :
     Nat → Option (List ZPoly)
@@ -8031,6 +8072,7 @@ def scaledRecombinationSearchMod
 /-- Size-`k` sublists of `xs`, each paired with its complement, order preserved
 in both components. The size-class building block of the size-ordered classical
 recombination search. -/
+@[expose]
 def subsetsOfSizeWithComplement {α : Type} : List α → Nat → List (List α × List α)
   | xs, 0 => [([], xs)]
   | [], _ + 1 => []
@@ -8041,6 +8083,7 @@ def subsetsOfSizeWithComplement {α : Type} : List α → Nat → List (List α
 /-- Sum of the degrees of a selected local-factor subset — the degree of the
 subset product whenever the leading coefficients do not cancel mod the lift
 modulus. -/
+@[expose]
 def selectedDegreeSum (sel : List ZPoly) : Nat :=
   sel.foldl (fun n g => n + g.degree?.getD 0) 0
 
@@ -8048,6 +8091,7 @@ def selectedDegreeSum (sel : List ZPoly) : Nat :=
 selected local-factor subset, computed with a running modular reduction so no
 intermediate value grows beyond `m`. Instantiated at the constant term and at
 the leading coefficient by `scaledCandidatePrefilter`. -/
+@[expose]
 def selectedProductResidue (coeffOf : ZPoly → Int) (sel : List ZPoly) (m : Nat) : Int :=
   centeredModNat (sel.foldl (fun acc g => acc * coeffOf g % (m : Int)) 1) m
 
@@ -8066,6 +8110,7 @@ pipeline (`polyProduct` / `centeredLiftPoly` / `dilate` / `primitivePart` /
 (`scaledCandidatePrefilter_eq_true_of_exactQuotient?_some` in the Mathlib
 layer), so pruning never changes the accepted-candidate sequence — only the
 wall-clock cost of rejecting a non-factor subset. -/
+@[expose]
 def scaledCandidatePrefilter
     (coreLc : Int) (target : ZPoly) (modulus : Nat) (sel : List ZPoly) : Bool :=
   let degSum := selectedDegreeSum sel
@@ -8094,6 +8139,7 @@ true recursion depth (`budget + (r+1)(2r+3)`: along any descent path the
 budget-decrementing steps are ≤ `budget` since `budget` threads monotonically, and
 the dispatch steps are ≤ `r·(2r+3)`), so it never cuts the search off early — the
 result is identical to the unfuelled search. -/
+@[expose]
 def scaledRecombinationSmartAux
     (coreLc : Int) (target : ZPoly) (modulus : Nat)
     (localFactors : List ZPoly) (budget : Nat) (fuel : Nat) : Option (List ZPoly) × Nat :=
@@ -8108,6 +8154,7 @@ def scaledRecombinationSmartAux
             scaledRecombinationSmartSizeLoop coreLc target modulus head tail
               (List.range (tail.length + 1)) budget fuel
 
+@[expose]
 def scaledRecombinationSmartSizeLoop
     (coreLc : Int) (target : ZPoly) (modulus : Nat) (head : ZPoly) (tail : List ZPoly)
     (sizes : List Nat) (budget : Nat) (fuel : Nat) : Option (List ZPoly) × Nat :=
@@ -8124,6 +8171,7 @@ def scaledRecombinationSmartSizeLoop
             | (none, b) =>
                 scaledRecombinationSmartSizeLoop coreLc target modulus head tail ds b fuel
 
+@[expose]
 def scaledRecombinationSmartCandLoop
     (coreLc : Int) (target : ZPoly) (modulus : Nat)
     (splits : List (List ZPoly × List ZPoly)) (budget : Nat) (fuel : Nat) :
@@ -8227,6 +8275,7 @@ The supplied `budget` is first tightened to `levelAwareSubsetBudget r budget`
 boundary it can finish instead of burning the rest of the budget partway into
 a level it cannot, since the partial level adds nothing to the declined
 verdict. Small-`r` searches (every level fits) see the budget unchanged. -/
+@[expose]
 def scaledRecombinationSmart
     (coreLc : Int) (f : ZPoly) (modulus : Nat) (localFactors : List ZPoly)
     (budget : Nat := defaultSubsetBudget) : Option (List ZPoly) × RecombStats :=
@@ -8871,6 +8920,7 @@ integer core.  The exhaustive slow path still recombines against the original
 primitive core, but the lift stage sees the monic polynomial required by the
 Hensel pipeline.
 -/
+@[expose]
 def toMonicLiftData
     (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) : LiftData :=
   henselLiftData (toMonic core).monic
@@ -8897,6 +8947,7 @@ divide `core` directly with no dilation.  It is monic over ℤ when
 `gcd(leadingCoeff core, p ^ k) = 1` and `core` is nonconstant
 (`monicTarget_monic`).
 -/
+@[expose]
 def monicTarget (core : ZPoly) (p k : Nat) : ZPoly :=
   reduceModPow (DensePoly.scale (leadingCoeffInverse core p k) core) p k
 
@@ -8908,6 +8959,7 @@ leading-coefficient-normalised `monicTarget` rather than the `x ↦ x/ℓf` dila
 `(toMonic core).monic`.  The lifted factors therefore divide `core` in
 `(ℤ/p^a)[x]` directly, and the CLD lattice runs over `core`'s own coordinate.
 -/
+@[expose]
 def coreLiftData
     (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) : LiftData :=
   henselLiftData (monicTarget core primeData.p (precisionForCoeffBound B primeData.p))
@@ -9015,6 +9067,7 @@ BHKS coefficient bound of the monic transform `(toMonic core).monic`: then
 `2·bhksCoeffBound (toMonic core).monic j < p ^ (precisionForCoeffBound k p)`
 holds for every coordinate `j`.  The floor is independent of the prime.
 -/
+@[expose]
 def cldCoeffFloor (core : ZPoly) : Nat :=
   let monicCore := (ZPoly.toMonic core).monic
   let n := monicCore.degree?.getD 0
@@ -9602,6 +9655,7 @@ modular factor data is the Berlekamp-form mod-`p` factorisation of
 `(toMonic core).monic`, the polynomial that `toMonicLiftData` passes to
 `henselLiftData`, so the Hensel seeds match the lift target (#8519, #8533).
 -/
+@[expose]
 def toMonicPrimeData? (core : ZPoly) : Option PrimeChoiceData :=
   choosePrimeData? (toMonic core).monic
 
@@ -9658,6 +9712,7 @@ subset recombination via `scaledRecombinationSmart`. Returns `none` when the sub
 before the search completes — an *untrustworthy* "no split" that the cost-based
 dispatcher routes to the lattice tier rather than reporting as irreducible. A
 genuine irreducible core (search completed within budget) returns `some #[core]`. -/
+@[expose]
 def classicalCoreFactorsWithBound
     (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) : Option (Array ZPoly) :=
   if B = 0 then
@@ -9676,6 +9731,7 @@ def classicalCoreFactorsWithBound
 
 /-- Raw factor array for the classical small-`r` tier. Declines (`none`) on no
 admissible prime or subset-budget exhaustion. -/
+@[expose]
 def factorClassicalFactorsWithBound (f : ZPoly) (B : Nat) : Option (Array ZPoly) :=
   let normalized := normalizeForFactor f
   if normalized.squareFreeCore.degree?.getD 0 = 0 then
@@ -9856,6 +9912,7 @@ constant/quadratic-root short-circuits as the classical tier; the residual
 exhaustive branch dispatches to the standalone integer trial-division core
 (`exhaustiveIntegerTrialCoreFactorsWithBound`). This is the trial-division
 tier of the three-tier `factor` combinator (SPEC PR #6580). -/
+@[expose]
 def factorTrialFactorsWithBound (f : ZPoly) (B : Nat) : Array ZPoly :=
   let normalized := normalizeForFactor f
   if normalized.squareFreeCore.degree?.getD 0 = 0 then
@@ -10041,6 +10098,7 @@ CLD path would treat this partition as `degenerate` and decline, which is why
 such a path "misses" on Swinnerton-Dyer inputs; the lattice tier uses this predicate, both
 in `latticeCoreLoop`'s early stop and in the trailing cap check, to turn the
 declined-but-certified case into a positive irreducibility verdict.) -/
+@[expose]
 def bhksSingleAllOnesPartition (f : ZPoly) (d : LiftData) : Bool :=
   -- Monic (`M2`) coordinate, matching `bhksRecoverClassified` (#8519).
   let L := bhksLatticeBasis (ZPoly.toMonic f).monic d.p d.k d.liftedFactors
@@ -10202,6 +10260,7 @@ trailing cap check requires `bhksRecoveryFloorGate core ≤ B` — below the flo
 all-ones partition may merely mean the lattice has not separated the factors
 yet, so certifying there would be unsound.  The public `factorLattice` supplies
 `latticePrecisionCap`, which clears the floor by construction. -/
+@[expose]
 def latticeCoreFactorsWithBound
     (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) : Option (Array ZPoly) :=
   if primeData.factorsModP.size ≤ 1 then
@@ -10813,6 +10872,7 @@ Constants are checked by integer primality. Positive-degree polynomials are
 checked from the returned `Factorization`: the scalar must be a unit and there
 must be exactly one polynomial factor with multiplicity one.
 -/
+@[expose]
 def isIrreducible (f : ZPoly) : Bool :=
   if f = 0 then
     false
diff --git a/HexBerlekampZassenhausMathlib.lean b/HexBerlekampZassenhausMathlib.lean
index 826034e74..deb045eef 100644
--- a/HexBerlekampZassenhausMathlib.lean
+++ b/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
diff --git a/HexBerlekampZassenhausMathlib/Basic.lean b/HexBerlekampZassenhausMathlib/Basic.lean
index bf8f0d026..7718d858a 100644
--- a/HexBerlekampZassenhausMathlib/Basic.lean
+++ b/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 :
diff --git a/HexBerlekampZassenhausMathlib/CLDColumnBound.lean b/HexBerlekampZassenhausMathlib/CLDColumnBound.lean
index fc034f795..5fa59b9a5 100644
--- a/HexBerlekampZassenhausMathlib/CLDColumnBound.lean
+++ b/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).
diff --git a/HexBerlekampZassenhausMathlib/CertReify.lean b/HexBerlekampZassenhausMathlib/CertReify.lean
index b85387685..61873bea7 100644
--- a/HexBerlekampZassenhausMathlib/CertReify.lean
+++ b/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
diff --git a/HexBerlekampZassenhausMathlib/FactorSoundness.lean b/HexBerlekampZassenhausMathlib/FactorSoundness.lean
index 03dd2c794..9cd1ab8d3 100644
--- a/HexBerlekampZassenhausMathlib/FactorSoundness.lean
+++ b/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`
diff --git a/HexBerlekampZassenhausMathlib/IntReductionMod.lean b/HexBerlekampZassenhausMathlib/IntReductionMod.lean
index 545534709..c6c5a1be6 100644
--- a/HexBerlekampZassenhausMathlib/IntReductionMod.lean
+++ b/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
diff --git a/HexBerlekampZassenhausMathlib/IrreducibleCert.lean b/HexBerlekampZassenhausMathlib/IrreducibleCert.lean
index 1943df3ba..c73ae0616 100644
--- a/HexBerlekampZassenhausMathlib/IrreducibleCert.lean
+++ b/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,7 +40,7 @@ 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)
@@ -41,18 +48,18 @@ private unsafe def evalZPolyUnsafe (e : Expr) :
     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 &&
diff --git a/HexBerlekampZassenhausMathlib/IrreducibleCertTest.lean b/HexBerlekampZassenhausMathlib/IrreducibleCertTest.lean
index d50890e8b..edb015b87 100644
--- a/HexBerlekampZassenhausMathlib/IrreducibleCertTest.lean
+++ b/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
diff --git a/HexBerlekampZassenhausMathlib/Lattice.lean b/HexBerlekampZassenhausMathlib/Lattice.lean
index 9b78c3079..37fece1da 100644
--- a/HexBerlekampZassenhausMathlib/Lattice.lean
+++ b/HexBerlekampZassenhausMathlib/Lattice.lean
@@ -4,9 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexBerlekampZassenhausMathlib.Basic
-import HexBerlekampZassenhausMathlib.SignatureClasses
-import HexLLLMathlib.ShortVector
+module
+
+public import HexBerlekampZassenhausMathlib.Basic
+public import HexBerlekampZassenhausMathlib.SignatureClasses
+public import HexLLLMathlib.ShortVector
+
+public section
+set_option backward.proofsInPublic true
+set_option backward.privateInPublic true
 
 /-!
 BHKS lattice-side objects for the van Hoeij `W ⊆ L'` adequacy (#8519).
@@ -48,6 +54,7 @@ def projectedRowsIntMatrix (L : Hex.BhksProjectedRows) :
   fun i j => (L.projectedRows.getD i.val #[]).getD j.val 0
 
 /-- The projected rational rows of the executable BHKS cut as a Mathlib matrix. -/
+@[expose]
 def projectedRowsRatMatrix (L : Hex.BhksProjectedRows) :
     Matrix (Fin L.projectedRows.size) (Fin L.factorCount) ℚ :=
   fun i j => ((L.projectedRows.getD i.val #[]).getD j.val 0 : ℚ)
@@ -56,6 +63,7 @@ def projectedRowsRatMatrix (L : Hex.BhksProjectedRows) :
 The integer row span represented by the executable projected BHKS rows.  This
 is the proof-facing `L' <= Z^r`.
 -/
+@[expose]
 def projectedRowSpanInt (L : Hex.BhksProjectedRows) :
     Submodule ℤ (Fin L.factorCount → ℤ) :=
   Submodule.span ℤ (Set.range fun i : Fin L.projectedRows.size =>
@@ -65,16 +73,19 @@ def projectedRowSpanInt (L : Hex.BhksProjectedRows) :
 The rational row space represented by the same executable projected rows.  This
 is the row-space input used by the RREF equivalence-class stage.
 -/
+@[expose]
 def projectedRowSpaceRat (L : Hex.BhksProjectedRows) :
     Submodule ℚ (Fin L.factorCount → ℚ) :=
   Submodule.span ℚ (Set.range fun i : Fin L.projectedRows.size =>
     Matrix.row (projectedRowsRatMatrix L) i)
 
 /-- Cast an integer vector over the lifted-factor indices to a rational vector. -/
+@[expose]
 def intVectorToRat {r : Nat} (v : Fin r → ℤ) : Fin r → ℚ :=
   fun i => (v i : ℚ)
 
 /-- A `0/1` indicator vector for a support of lifted factor indices. -/
+@[expose]
 def indicatorVector {r : Nat} (S : Set (Fin r)) : Fin r → ℤ :=
   by
     classical
@@ -156,6 +167,7 @@ rather than the raw array size so it remains well-typed for abstract
 `BhksLatticeBasis` values; `TrueFactorLift.basis_eq` ties these together for
 the executable basis.
 -/
+@[expose]
 def supportProduct (L : Hex.BhksLatticeBasis) (S : LiftedFactorSupport L) :
     Hex.ZPoly :=
   by
@@ -171,6 +183,7 @@ pre-indicator column-`j` entry of the true-factor CLD vector; the centering
 (`psiCut`) and indicator weighting are layered on top by the tight-column work
 (`#7651`).
 -/
+@[expose]
 def supportCldSum (L : Hex.BhksLatticeBasis) (S : LiftedFactorSupport L)
     (f : Hex.ZPoly) (p a : Nat) : Hex.ZPoly :=
   by
@@ -269,6 +282,7 @@ This holds definitionally for `Hex.bhksLatticeBasis` (see
 `bhksLatticeBasis_blockForm`) and is the only fact the canonical coordinate
 producers need about the basis.
 -/
+@[expose]
 def BhksBlockForm (L : Hex.BhksLatticeBasis) : Prop :=
   L.basis =
     Hex.Matrix.ofFn
@@ -372,12 +386,14 @@ theorem precision_eq
 
 end RecoveredLift
 
+@[expose]
 def supportEquivalent {r : Nat} (trueSupports : Set (Set (Fin r)))
     (j k : Fin r) : Prop :=
   ∀ S ∈ trueSupports, (j ∈ S ↔ k ∈ S)
 
 /-- Nat-indexed form of `supportEquivalent`, convenient for filtering
 `List.range r` while retaining proof irrelevance for the bounds. -/
+@[expose]
 def supportEquivalentAt {r : Nat} (trueSupports : Set (Set (Fin r)))
     (j k : Nat) : Prop :=
   ∃ (hj : j < r) (hk : k < r),
@@ -418,6 +434,7 @@ theorem supportEquivalentAt_trans {r : Nat}
 
 /-- Minimum representatives of support-equivalence classes, emitted in
 ascending column order. -/
+@[expose]
 def supportRepresentativeColumns {r : Nat}
     (trueSupports : Set (Set (Fin r))) : List Nat :=
   by
@@ -437,12 +454,14 @@ def supportClassMembers {r : Nat}
       (fun j => decide (supportEquivalentAt trueSupports j rep))
 
 /-- Canonical partition of columns by true-support membership signatures. -/
+@[expose]
 def supportPartitionByMinColumn {r : Nat}
     (trueSupports : Set (Set (Fin r))) : List (List Nat) :=
   (supportRepresentativeColumns trueSupports).map
     (fun rep => supportClassMembers trueSupports rep)
 
 /-- The executable indicator-array shape for a finite Nat-indexed class. -/
+@[expose]
 def classIndicatorArray (r : Nat) (members : List Nat) : Array Int :=
   ((List.range r).map (fun i => if i ∈ members then (1 : Int) else 0)).toArray
 
@@ -722,6 +741,7 @@ stores the projected rows.
 -/
 
 /-- Projection onto the first `r` coordinates as a `ℤ`-linear map. -/
+@[expose]
 def projFirst (r n : Nat) : (Fin (r + n) → ℤ) →ₗ[ℤ] (Fin r → ℤ) where
   toFun w := fun i => w (Fin.castAdd n i)
   map_add' a b := by funext i; simp
diff --git a/HexBerlekampZassenhausMathlib/LatticeTier.lean b/HexBerlekampZassenhausMathlib/LatticeTier.lean
index d5a27719b..6adf7e4df 100644
--- a/HexBerlekampZassenhausMathlib/LatticeTier.lean
+++ b/HexBerlekampZassenhausMathlib/LatticeTier.lean
@@ -4,12 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexBerlekampZassenhausMathlib.IntReductionMod
-import HexBerlekampZassenhausMathlib.CLDColumnBound
-import HexBerlekampZassenhausMathlib.Recovery
-import HexBerlekampZassenhausMathlib.PartitionRefinement
-import HexGramSchmidtMathlib.Int.Swap
-import HexLLLMathlib.ShortVector
+module
+
+public import HexBerlekampZassenhausMathlib.IntReductionMod
+public import HexBerlekampZassenhausMathlib.CLDColumnBound
+public import HexBerlekampZassenhausMathlib.Recovery
+public import HexBerlekampZassenhausMathlib.PartitionRefinement
+public import HexGramSchmidtMathlib.Int.Swap
+public import HexLLLMathlib.ShortVector
+
+public section
+set_option backward.proofsInPublic true
+set_option backward.privateInPublic true
 
 /-!
 # Irreducibility of the van Hoeij / CLD lattice tier (#8417)
diff --git a/HexBerlekampZassenhausMathlib/PartitionRefinement.lean b/HexBerlekampZassenhausMathlib/PartitionRefinement.lean
index 7f6d6f45e..2b979fecf 100644
--- a/HexBerlekampZassenhausMathlib/PartitionRefinement.lean
+++ b/HexBerlekampZassenhausMathlib/PartitionRefinement.lean
@@ -4,8 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexBerlekampZassenhausMathlib.Recovery
-import HexBerlekampZassenhausMathlib.Basic
+module
+
+public import HexBerlekampZassenhausMathlib.Recovery
+public import HexBerlekampZassenhausMathlib.Basic
+
+public section
+set_option backward.proofsInPublic true
+set_option backward.privateInPublic true
 
 /-!
 Support-partition counting for the BHKS class-count lower bound (#8519).
diff --git a/HexBerlekampZassenhausMathlib/Recovery.lean b/HexBerlekampZassenhausMathlib/Recovery.lean
index 5f73b90c8..b698ed155 100644
--- a/HexBerlekampZassenhausMathlib/Recovery.lean
+++ b/HexBerlekampZassenhausMathlib/Recovery.lean
@@ -4,8 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexBerlekampZassenhausMathlib.Lattice
-import HexBerlekampZassenhausMathlib.SignatureClasses
+module
+
+public import HexBerlekampZassenhausMathlib.Lattice
+public import HexBerlekampZassenhausMathlib.SignatureClasses
+
+public section
+set_option backward.proofsInPublic true
+set_option backward.privateInPublic true
 
 /-!
 Executable class-count semantics for the BHKS equivalence-class indicators
diff --git a/HexBerlekampZassenhausMathlib/SignatureClasses.lean b/HexBerlekampZassenhausMathlib/SignatureClasses.lean
index c3df8dae2..a5a8fa684 100644
--- a/HexBerlekampZassenhausMathlib/SignatureClasses.lean
+++ b/HexBerlekampZassenhausMathlib/SignatureClasses.lean
@@ -4,9 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexBerlekampZassenhaus
-import Mathlib.Data.Nat.Find
-import HexRowReduceMathlib.RankSpanNullspace
+module
+
+public import HexBerlekampZassenhaus
+public import Mathlib.Data.Nat.Find
+public import HexRowReduceMathlib.RankSpanNullspace
+
+public section
+set_option backward.proofsInPublic true
+set_option backward.privateInPublic true
 
 /-!
 Partition semantics for the executable `bhksInsertSignatureClass` fold.
@@ -37,6 +43,7 @@ Representative columns for the `sig j = sig k` equivalence on
 `{0, …, r-1}`: the columns whose signature has not been seen at any
 earlier column. The list is ascending by construction.
 -/
+@[expose]
 def representativeColumns (r : Nat) (sig : Nat → Array Rat) : List Nat :=
   (List.range r).filter
     (fun j => ((List.range j).filter (fun k => sig k = sig j)).isEmpty)
@@ -47,6 +54,7 @@ class per representative column, listing exactly the columns with the
 same signature as that representative.  Classes appear in ascending
 representative order; each class's member list is ascending.
 -/
+@[expose]
 def partitionByMinColumn (r : Nat) (sig : Nat → Array Rat) : List (List Nat) :=
   (representativeColumns r sig).map
     (fun rep => (List.range r).filter (fun j => sig j = sig rep))
diff --git a/HexBerlekampZassenhausMathlib/UFDPartition.lean b/HexBerlekampZassenhausMathlib/UFDPartition.lean
index 4d90804c3..cc3a3b0f7 100644
--- a/HexBerlekampZassenhausMathlib/UFDPartition.lean
+++ b/HexBerlekampZassenhausMathlib/UFDPartition.lean
@@ -4,12 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import Mathlib.Algebra.Polynomial.BigOperators
-import Mathlib.Algebra.Polynomial.FieldDivision
-import Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
-import Mathlib.Algebra.EuclideanDomain.Int
-import Mathlib.Algebra.Squarefree.Basic
-import Mathlib.RingTheory.Polynomial.UniqueFactorization
+module
+
+public import Mathlib.Algebra.Polynomial.BigOperators
+public import Mathlib.Algebra.Polynomial.FieldDivision
+public import Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
+public import Mathlib.Algebra.EuclideanDomain.Int
+public import Mathlib.Algebra.Squarefree.Basic
+public import Mathlib.RingTheory.Polynomial.UniqueFactorization
+
+public section
+set_option backward.proofsInPublic true
+set_option backward.privateInPublic true
 
 /-!
 Abstract UFD partition-cardinality bound used by the BHKS Group B
diff --git a/HexHensel/Basic.lean b/HexHensel/Basic.lean
index b6d9bee75..0bd22b3e8 100644
--- a/HexHensel/Basic.lean
+++ b/HexHensel/Basic.lean
@@ -268,6 +268,7 @@ namespace FpPoly
 variable {p : Nat} [ZMod64.Bounds p]
 
 /-- Lift `F_p` coefficients to their standard nonnegative integer representatives. -/
+@[expose]
 def liftToZ (f : FpPoly p) : ZPoly :=
   DensePoly.ofCoeffs <|
     (List.range f.size).map (fun i => Int.ofNat (f.coeff i).toNat) |>.toArray
diff --git a/HexHensel/Multifactor.lean b/HexHensel/Multifactor.lean
index 6871270be..c00d4e77f 100644
--- a/HexHensel/Multifactor.lean
+++ b/HexHensel/Multifactor.lean
@@ -36,6 +36,7 @@ namespace ZPoly
 Extended gcd witnesses scaled so their Bezout combination is monic when the
 raw Euclidean gcd is a nonzero constant unit.
 -/
+@[expose]
 def normalizedXGCD
     (p : Nat) [ZMod64.Bounds p]
     (g h : ZPoly) : DensePoly.XGCDResult (ZMod64 p) :=
diff --git a/HexHensel/QuadraticMultifactor.lean b/HexHensel/QuadraticMultifactor.lean
index b6d772243..bf89a1f9b 100644
--- a/HexHensel/QuadraticMultifactor.lean
+++ b/HexHensel/QuadraticMultifactor.lean
@@ -612,6 +612,7 @@ Consumed by `quadraticMultifactorLiftInvariant_of_factorsModP`: the
 per-split `gcd = 1` lifts via `normalizedXGCD_liftToZ_bezout_congr_of_gcd_eq_one`
 into the Bezout half of `QuadraticLiftLoopInvariant`.
 -/
+@[expose]
 def QuadraticMultifactorCoprimeSplits
     (p : Nat) [ZMod64.Bounds p] : List (FpPoly p) → Prop
   | [] => True
diff --git a/HexPolyZMathlib/Mignotte.lean b/HexPolyZMathlib/Mignotte.lean
index f2f09d626..eb3fd4679 100644
--- a/HexPolyZMathlib/Mignotte.lean
+++ b/HexPolyZMathlib/Mignotte.lean
@@ -41,6 +41,7 @@ private theorem range_foldl_add_eq_finset_sum_nat (g : Nat → Nat) (m : Nat) :
       rw [ih, Finset.sum_range_succ]
 
 /-- The Euclidean norm of the coefficient vector of an integer polynomial. -/
+@[expose]
 def l2norm (f : Polynomial ℤ) : ℝ :=
   Real.sqrt (∑ i ∈ f.support, (f.coeff i : ℝ) ^ 2)
 
diff --git a/progress/20260704T141029Z_bz-mathlib-module-migration-phase1b.md b/progress/20260704T141029Z_bz-mathlib-module-migration-phase1b.md
new file mode 100644
index 000000000..e5f52f4df
--- /dev/null
+++ b/progress/20260704T141029Z_bz-mathlib-module-migration-phase1b.md
@@ -0,0 +1,52 @@
+# BZ Mathlib bridge module-system migration (Phase 1b, #8598)
+
+## Accomplished
+Migrated `HexBerlekampZassenhausMathlib/` (13 files + umbrella) onto the
+Lean 4 module system, the Phase-1b follow-up to #8597 (executable side).
+
+Per file: `module`, `import X` -> `public import X`, `public section` +
+`set_option backward.{proofsInPublic,privateInPublic} true` where private
+decls are referenced in public. Then the exposure/meta work:
+
+- **`@[expose]` pass (89 defs).** Exported `rfl`/`simp`/`unfold`/`change`/
+  `decide`/`rw`-on-def proofs in the bridge reduce through executable and
+  Mathlib-side defs; each surfaced as "Expected a definition with an exposed
+  body" / "not unfolded because not exposed" / "not an inductive datatype".
+  Exposed the flagged defs at their definition sites, driven outward from the
+  first error until green. Sites span the executable `HexBerlekampZassenhaus/
+  Basic.lean` (the bulk), `HexHensel/{Basic,Multifactor,QuadraticMultifactor}`,
+  the Mathlib-side `HexBerlekampMathlib/Basic.lean` (`fpPolyEquiv`,
+  `toMathlibPolynomial`), `HexPolyZMathlib/Mignotte.lean` (`l2norm`), and the
+  bridge's own `Basic`/`Lattice`/`SignatureClasses`.
+- **Meta tactic files.** `IrreducibleCert.lean` needed
+  `public meta import ...CertReify` and its eval/match helpers marked `meta`
+  (they run at elaboration inside the `irreducible_cert` elaborator);
+  `IrreducibleCertTest.lean` needed `public meta import ...IrreducibleCert`
+  and `roundTrips` marked `meta`.
+- **Certificate kernel replay.** The `irreducible_cert` proofs attach
+  `Eq.refl true` per certificate check, so the kernel must reduce
+  `checkIrreducibleCertLinear` and its Berlekamp pow-chain replay plus the
+  `Array`/`DensePoly` `==` comparisons. Handled in `IrreducibleCertTest.lean`
+  with `import all HexBerlekampZassenhaus.Basic`, `import all
+  HexBerlekamp.Irreducibility`, and `import all Init.Data.Array.DecidableEq`
+  (the recipe's kernel-reduction tool, mirroring the executable side).
+- **Two proof-text repairs**, both in the `monicModPImage`-zero branch of
+  `existsUnique_modPFactorSubset...` in `Basic.lean`: a `simp [hzero]` that
+  started leaving a spurious `SemigroupWithZero ?m` became `rw [if_pos hzero]`,
+  and `exact dvd_zero _` on `toMathlibPolynomial 0` now rewrites through an
+  inline `toMathlibPolynomial 0 = 0` (the file's `Polynomial.ext` idiom, since
+  `map_zero` does not synthesize on `fpPolyEquiv`). No theorem statements
+  changed.
+
+## Current frontier
+Full `lake build` green (4088 jobs), `HexBerlekampZassenhausMathlib` green,
+`HexConformance` green, BZ bench/emit exes green, `scripts/check_dag.py` exit 0,
+no `sorry`/`axiom`/`native_decide` in the diff.
+
+## Next step
+Second opinion, then open the PR. Phase 2 (splitting the 22k-line
+`HexBerlekampZassenhausMathlib/Basic.lean`) is now unblocked and tracked
+separately.
+
+## Blockers
+None.