# Integer polynomial factorization

`hex-berlekamp-zassenhaus` implements complete factorization of univariate
integer polynomials.  The executable library is Mathlib-free; its semantic,
completeness, and irreducibility proofs live in
`HexBerlekampZassenhausMathlib`.

The normative design is
[`HexBerlekampZassenhaus/SPEC/hex-berlekamp-zassenhaus.md`](HexBerlekampZassenhaus/SPEC/hex-berlekamp-zassenhaus.md).
This file is a short map for development work.

## Production route

`ZPoly.factorize` normalizes the input once, then dispatches through:

1. direct-coordinate classical recombination;
2. direct-coordinate CLD lattice recombination after a typed classical
   decline;
3. exhaustive integer trial division as the total backstop.

Both modular tiers share one `DirectPrimePlan` and one original-coordinate
recovery model. Each constructs the Hensel lift required by its own precision
bound from that cached modular factorization. Finite-field factors are monic
by convention, but the integral `toMonic` coordinate transform is not part of
the production route.

Every optional modular result is checked by exact product reconstruction
before the dispatcher accepts it.

## Executable modules

- `SquareFreeInput.lean` defines the primitive square-free problem indexed by every
  direct plan and lift.
- `PrimeSelection.lean`, `ChoosePrimeData.lean`, and
  `Modular/PrimePlan.lean` implement direct modular planning.
- `Hensel/DirectLift.lean` defines the plan-indexed recovery lift.
- `Classical/` contains the sole production classical search and its typed
  outcomes.
- `BhksCandidates.lean`, `BhksRecover.lean`, and `Lattice.lean` implement CLD
  construction, recovery, and the unconditional trial backstop.
- `Dispatch.lean` contains the public tier entry points and
  `ZPoly.factorize`, together with the typed dispatch result and trace.

`DirectFactorTrace` reports the tier, an optional typed classical decline, and
the `ClassicalStats` generated by the same run that produced the answer.

## Proof modules

The direct Hensel facts are in `Hensel/DirectLift.lean`.  Direct support and
CLD adequacy are organized around the mathematical objects they establish:

- `Lattice/DirectSupport.lean`;
- `Lattice/DirectRecovery.lean`;
- `Lattice/DirectAdequacy.lean`;
- `LatticeFactorization.lean`;
- `LatticeTotality.lean`.

The classical completeness proof is in `Classical/`.  General mathematical
objects are kept in:

- `FactorBound.lean`;
- `Factorization.lean`;
- `ModularPolynomial.lean`;
- `IrreducibilityCertificate.lean`;
- `ModPPartition.lean`.

There is no generic “public surface” module and no duplicate monic-coordinate
CLD recovery stack.

## Validation

Run:

```text
lake build
```

Then run the existing Berlekamp–Zassenhaus conformance/oracle check, benchmark
import lint, and benchmark verification check. Changes to the factorizer also
rerun the public Hex rows of the stored polynomial-factorization corpus
comparison. Recorded external-system observations are not rerun merely because
Hex changes.

Never introduce an axiom or `native_decide`.  Do not replace proof obligations
with `sorry`.