27.8. Result and correctness🔗

structure

Hex.Factorization : Type
Hex.Factorization : Type

Public factorization result for an integer polynomial Hex.ZPoly.

The scalar carries the input's signed content: for nonzero inputs this is sign(lc f) * ZPoly.content f, while zero inputs use scalar 0. Polynomial factors are primitive, positive-leading-coefficient factors stored with explicit multiplicities; factor order remains operational, with the mathematical contract expressed by multiplying the scalar and stored factors.

Constructor

Hex.Factorization.mk

Fields

scalar : ℤ

Signed scalar absorbing both sign and integer content.

factors : Array (Hex.ZPoly × ℕ)

Polynomial factors paired with explicit positive multiplicities.

def

Hex.ZPoly.factorize (f : Hex.ZPoly) : Hex.Factorization
Hex.ZPoly.factorize (f : Hex.ZPoly) :
  Hex.Factorization

The public total factorisation of a Hex.ZPoly.

Small modular supports use Hex.factorClassical. Large supports reuse one Hensel lift for repeated exact low-cardinality peeling. Once peeling makes exact progress, a selected-column CLD proposal partitions the hard residual; otherwise the speculative tier is skipped. Every proposed piece is checked and factored again by the proved classical method. If the proposal declines, Hex.factorLattice tries full CLD recombination. Hex.factorTrial is the total backstop. It does not depend on Hex.choosePrimeData?, so this function still returns a factorisation when prime selection fails.

This definition lives in the Hex.ZPoly namespace, so it can be called with dot notation as f.factorize.

For a nonzero input, the result has signed content as its scalar; positive multiplicities; primitive, irreducible factors with positive leading coefficients; and no two associated factor entries. Its product is the input, and this normalized factorization is unique. The next section states those guarantees as theorems.

Hex.factorTraced returns the same factorization together with the selected Hex.FactorMethod, a possible classical decline, and measurements of the classical search. The trace is observational: all methods are checked by the same product and irreducibility theorems.