Skip to content

DEV.md

Latest commit

 

History

History
85 lines (64 loc) · 3.06 KB

DEV.md

File metadata and controls

85 lines (64 loc) · 3.06 KB
Raw

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. 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:

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.