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

theorem

HexBerlekampZassenhausMathlib.factorize_normalized (f : Hex.ZPoly)
  (hf : f ≠ 0) :
  f.factorize.product = f ∧
    (∀ entry ∈ f.factorize.factors,
        entry.1.Primitive ∧
          Irreducible (HexPolyZMathlib.toPolynomial entry.1) ∧
            0 < Hex.DensePoly.leadingCoeff entry.1) ∧
      (∀ entry ∈ f.factorize.factors, 0 < entry.2) ∧
        List.Pairwise
            (fun a b =>
              ¬Associated (HexPolyZMathlib.toPolynomial a.1)
                  (HexPolyZMathlib.toPolynomial b.1))
            f.factorize.factors.toList ∧
          f.factorize.scalar =
            if f = 0 then 0
            else
              if Hex.DensePoly.leadingCoeff f < 0 then -f.content
              else f.content
HexBerlekampZassenhausMathlib.factorize_normalized
  (f : Hex.ZPoly) (hf : f ≠ 0) :
  f.factorize.product = f ∧
    (∀ entry ∈ f.factorize.factors,
        entry.1.Primitive ∧
          Irreducible
              (HexPolyZMathlib.toPolynomial
                entry.1) ∧
            0 <
              Hex.DensePoly.leadingCoeff
                entry.1) ∧
      (∀ entry ∈ f.factorize.factors,
          0 < entry.2) ∧
        List.Pairwise
            (fun a b =>
              ¬Associated
                  (HexPolyZMathlib.toPolynomial
                    a.1)
                  (HexPolyZMathlib.toPolynomial
                    b.1))
            f.factorize.factors.toList ∧
          f.factorize.scalar =
            if f = 0 then 0
            else
              if
                  Hex.DensePoly.leadingCoeff
                      f <
                    0 then
                -f.content
              else f.content

The normalized irreducible factorization produced for a nonzero polynomial.

The product reconstructs the input. Every recorded factor is primitive, has positive leading coefficient, and is irreducible after transport to Polynomial ℤ; multiplicities are positive; distinct entries are not associates; and the scalar is the signed content of the input.

The hypothesis f ≠ 0 is necessary because the factorization of zero is degenerate: its scalar and product are zero, while zero is not primitive.

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.