27.9. The Mathlib correspondence🔗

Everything above is executable and Mathlib-free. HexBerlekampZassenhausMathlib is the companion that restates the guarantees of Hex.ZPoly.factorize against Mathlib's Polynomial ℤ, transported through HexPolyZMathlib.toPolynomial.

The product identity holds unconditionally and is re-exported as a simp lemma:

theorem

HexBerlekampZassenhausMathlib.factorize_product (f : Hex.ZPoly) :
  f.factorize.product = f
HexBerlekampZassenhausMathlib.factorize_product
  (f : Hex.ZPoly) :
  f.factorize.product = f

The default executable factorization multiplies back to the input.

Every emitted factor is irreducible, with no hypothesis on the input:

theorem

HexBerlekampZassenhausMathlib.factorize_irreducible_of_nonUnit
  (f : Hex.ZPoly) (entry : Hex.ZPoly × ℕ) :
  entry ∈ f.factorize.factors → entry.1.Irreducible
HexBerlekampZassenhausMathlib.factorize_irreducible_of_nonUnit
  (f : Hex.ZPoly)
  (entry : Hex.ZPoly × ℕ) :
  entry ∈ f.factorize.factors →
    entry.1.Irreducible

Every polynomial factor emitted by the default executable factorization is irreducible in the executable Hex.ZPoly sense.

The headline theorem bundles the full normal form of a nonzero input's factorization:

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.

That normal form is canonical. Any two factorizations satisfying it with the same product agree up to the packing of multiplicities:

theorem

HexBerlekampZassenhausMathlib.factorize_unique (φ ψ : Hex.Factorization)
  (hφ_norm :
    ∀ entry ∈ φ.factors, Hex.normalizeFactorSign entry.1 = entry.1)
  (hψ_norm :
    ∀ entry ∈ ψ.factors, Hex.normalizeFactorSign entry.1 = entry.1)
  (hφ_nonconst :
    ∀ entry ∈ φ.factors, 0 < Hex.DensePoly.natDegree entry.1)
  (hψ_nonconst :
    ∀ entry ∈ ψ.factors, 0 < Hex.DensePoly.natDegree entry.1)
  (hφ_irr : ∀ entry ∈ φ.factors, entry.1.Irreducible)
  (hψ_irr : ∀ entry ∈ ψ.factors, entry.1.Irreducible)
  (hφ_prod_ne : φ.product ≠ 0) (hprod : φ.product = ψ.product) :
  φ.scalar = ψ.scalar ∧
    (List.map (fun e => Multiset.replicate e.2 e.1)
          φ.factors.toList).sum =
      (List.map (fun e => Multiset.replicate e.2 e.1)
          ψ.factors.toList).sum
HexBerlekampZassenhausMathlib.factorize_unique
  (φ ψ : Hex.Factorization)
  (hφ_norm :
    ∀ entry ∈ φ.factors,
      Hex.normalizeFactorSign entry.1 =
        entry.1)
  (hψ_norm :
    ∀ entry ∈ ψ.factors,
      Hex.normalizeFactorSign entry.1 =
        entry.1)
  (hφ_nonconst :
    ∀ entry ∈ φ.factors,
      0 < Hex.DensePoly.natDegree entry.1)
  (hψ_nonconst :
    ∀ entry ∈ ψ.factors,
      0 < Hex.DensePoly.natDegree entry.1)
  (hφ_irr :
    ∀ entry ∈ φ.factors,
      entry.1.Irreducible)
  (hψ_irr :
    ∀ entry ∈ ψ.factors,
      entry.1.Irreducible)
  (hφ_prod_ne : φ.product ≠ 0)
  (hprod : φ.product = ψ.product) :
  φ.scalar = ψ.scalar ∧
    (List.map
          (fun e =>
            Multiset.replicate e.2 e.1)
          φ.factors.toList).sum =
      (List.map
          (fun e =>
            Multiset.replicate e.2 e.1)
          ψ.factors.toList).sum

Two irreducible executable factorizations of the same nonzero polynomial have the same signed scalar and the same multiplicity-flattened multiset of polynomial factors. The corrected statement compares flattened normalized factors rather than raw List.Perm, since Hex.Factorization does not constrain factor sign, multiplicity packing, or constant factors. The normalizeFactorSign and nonconst hypotheses rule out the corresponding counterexamples.

The companion also carries the tactic surface across the boundary. The base library's factor_poly and irreducibility elaborators work on Hex.ZPoly goals; importing HexBerlekampZassenhausMathlib upgrades them to accept Polynomial ℤ as well, and adds the kernel-checked factor_poly! and irreducibility! variants whose certificate checks reduce inside the kernel.