refactor(bz): split the BerlekampZassenhaus Basic.lean monoliths into dependency-ordered modules

[kim-em]

Phase 2 of the Berlekamp-Zassenhaus reorganization: split the two oversized Basic.lean files into small, one-subject modules. This is the original goal; Phases 1a (#8597, landed) and 1b (#8598) migrate the two libraries onto the module system first, which this split depends on.

Prerequisite: both #8597 and #8598 must be merged (both libraries on the module system) before starting.

Targets

• HexBerlekampZassenhaus/Basic.lean — ~19,130 lines -> ~16 leaves.
• HexBerlekampZassenhausMathlib/Basic.lean — ~22,707 lines -> ~15 leaves.

Aim for ~1000-1500 lines per module, hard ceiling 3000.

Method (HexLLL #8448 template, module-system style)

For each monolith:

1. Carve cohesive declaration clusters into new sibling .lean files under the library directory. Each leaf: module / public import <sibling deps> (+ import all <sibling> where it needs that sibling's private helpers) / public section / re-open the enclosing namespace (and noncomputable section + open Polynomial for the Mathlib file) / docstring.
2. Delete Basic.lean (no compatibility shim). Repoint importers: the umbrella public imports every new leaf; in-library siblings that imported .Basic import the specific leaves they need (not the umbrella — that would cycle); external consumers (bench, conformance, HexManual/Tutorials/Coppersmith.lean, reports/scratch/*) change import ...Basic -> import HexBerlekampZassenhaus / import HexBerlekampZassenhausMathlib.
3. Move clusters top-down, one at a time, running lake build after each so the tree never sits broken.

Invariants

• Each file is one Lean module = a strictly linear order; the split is a topological cut. Re-open namespaces per leaf (the executable file re-opens ZPoly 7x, etc.).
• mutual blocks are atomic (executable: six; Mathlib: two).
• A ...Proofs leaf sits after the leaf defining what it proves.
• Keep _of_bound / _of_primitive_pos_lc_core variant families together (Mathlib file).
• Keep helper lemmas private; reach them across leaves with import all Sibling (the established HexDeterminant idiom).

Proposed split A - HexBerlekampZassenhaus/Basic.lean (line ranges approximate)

Leaf	Lines	Subject
PrimeSelection	23-1366	X/xPower, good-prime predicates, small-prime primality, candidates, monic mod-p image, scoring & choosePrime
Records	1368-1784	data records, Factorization/product, normalization pipeline defs
Certificate	1785-2210	irreducibility-certificate structures, checkers, certifyIrreducible?
ChoosePrimeData	2212-3041	choosePrimeData?/Walk?/Score + correctness, henselLiftData
ReassemblyProofs	3051-4600	BHKS bounds; reassembly-correctness theorems
Lattice	4606-5493	trial/root candidate defs, centered-lift/CLD, BHKS lattice basis
BhksCandidates	5495-6948	bhksIndicatorCandidates?, dilate lemmas + candidate correctness
BhksRecover	6949-7873	bhksRecover?/coreRecover? + core-recover correctness
Recombination	7874-9603	recombination-search defs (mutual blocks) + Hensel precision
FactorEntryPoints	9605-10730	factorClassical/Trial/Lattice/factor + factor_scalar theorems
IrreducibleCore	10731-12030	Irreducible class, C/linear/size-two, main mod-p theorem
RecombineProofs	12035-13650	recombination + bhksRecover* correctness + core-factors specs
TrialProofs	14007-16290	trial-division + integer-root correctness
QuadraticRootProofs	16294-17540	quadratic-integer-root correctness
PrimitivityProofs	17544-18728	squareFreeCore/expandRepeatedPart/reassembly primitivity
ProductProofs	18729-19130	factorTrial_product, factor_product, checkIrreducibleCert_*

Proposed split B - HexBerlekampZassenhausMathlib/Basic.lean

Leaf	Lines	Subject
PublicSurface	31-1253	transport bounds, factor_product, factor_unique, checkIrreducibleCert_sound
ModPFactor	1255-2049	modPFactor/monicModPImage, ModPSubsetPartitionHypotheses
LiftedFactor	2050-3033	lifted-factor infra + candidate defs + Hensel-subset correspondence
M1Recovery	3034-4021	M1 recovery + Hensel-lift invariant + LiftedFactorSubsetPartition
RecombinationSplit	4022-5496	mask/list combinatorics bridging Finset subsets to executable enumeration
RecombinationCandidate	5497-6528	recombinationCandidate + candidate=factor lemmas
HenselFactorProps	6529-8695	monic-primitive helpers, henselLiftData props, factorsModP Berlekamp-form
SubsetCoprimality	8696-10046	choosePrimeData degree/injectivity + subset/complement coprimality
ForwardHenselTransport	10047-12368	forward Hensel transport for the canonical lifted subset
RecombinationMonic	12369-14316	monicness/squarefree of recombination candidate + degree-cover
PrimitivityDegreeCover	14317-15033	primitivity/leadingCoeff/normalizeFactorSign
ScaledSearchCoverage	15034-17321	scaled-tier search coverage, RecoveredScaledSearch
SmartSearchCoverage	17322-18829	size-ordered coverage; both mutual blocks; RecoveredSmartSearch
SearchAssembly	18830-20431	associated-factor lemmas + choosePrimeData partition assembly
MonicCorrespondent	20432-21731	ZPoly scale/dilate helpers + forward monic correspondent
ToMonicUniqueness	21734-22707	non-circular lift-stage subset-uniqueness core (#7474)

The three >2000-line Mathlib rows have marked optional finer cuts if everything must be <=1500.

Verify

lake build green after every cluster move (0 sorries); python scripts/check_dag.py; HexConformance; declaration count conserved (compare a grep -c of decl keywords on the old monolith vs summed over the new leaves + shim-less umbrella); git diff shows only moves + module boilerplate, no proof-logic deltas.

🤖 Prepared with Claude Code