24.8. The Mathlib correspondence🔗

These declarations describe the executable results in Mathlib terms. The central contract identifies the executable scalar with Mathlib's determinant-defined resultant:

theorem

Hex.DensePoly.toPolynomial_resultant.{u} {R : Type u} [CommRing R]
  [DecidableEq R] [Div R] [Hex.ExactDivLaws R] (f g : Hex.DensePoly R) :
  f.resultant g =
    (HexPolyMathlib.toPolynomial f).resultant
      (HexPolyMathlib.toPolynomial g) f.natDegree g.natDegree
Hex.DensePoly.toPolynomial_resultant.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] [Div R]
  [Hex.ExactDivLaws R]
  (f g : Hex.DensePoly R) :
  f.resultant g =
    (HexPolyMathlib.toPolynomial
          f).resultant
      (HexPolyMathlib.toPolynomial g)
      f.natDegree g.natDegree

The executable and Mathlib resultants agree under dense-polynomial correspondence, with the executable default formal degrees made explicit.

The executable discriminant has the same total zero/constant convention as Mathlib's determinant-defined discriminant:

theorem

Hex.DensePoly.toPolynomial_disc.{u} {R : Type u} [CommRing R]
  [DecidableEq R] [Div R] [Hex.ExactDivLaws R] (f : Hex.DensePoly R) :
  f.disc = (HexPolyMathlib.toPolynomial f).discr
Hex.DensePoly.toPolynomial_disc.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] [Div R]
  [Hex.ExactDivLaws R]
  (f : Hex.DensePoly R) :
  f.disc =
    (HexPolyMathlib.toPolynomial f).discr

The executable and Mathlib discriminants agree under dense-polynomial correspondence.

For positive-degree polynomials in characteristic zero, discriminants multiply with the square of the cross-resultant. The degree hypotheses exclude the nonunit-constant counterexample created by the total constant convention. Over a characteristic-zero field, nonvanishing is therefore the expected separability criterion:

theorem

Hex.DensePoly.disc_mul.{u} {R : Type u} [CommRing R] [IsDomain R]
  [IsAddTorsionFree R] [DecidableEq R] [Div R] [Hex.ExactDivLaws R]
  (f g : Hex.DensePoly R) (hf : 0 < f.natDegree)
  (hg : 0 < g.natDegree) :
  (f * g).disc = f.disc * g.disc * f.resultant g ^ 2
Hex.DensePoly.disc_mul.{u} {R : Type u}
  [CommRing R] [IsDomain R]
  [IsAddTorsionFree R] [DecidableEq R]
  [Div R] [Hex.ExactDivLaws R]
  (f g : Hex.DensePoly R)
  (hf : 0 < f.natDegree)
  (hg : 0 < g.natDegree) :
  (f * g).disc =
    f.disc * g.disc * f.resultant g ^ 2

Discriminants multiply with the square of the cross-resultant.

The positive-degree hypotheses are essential: Mathlib and the executable API assign discriminant one to constants, while multiplying by a nonunit constant scales the other discriminant.

theorem

Hex.DensePoly.disc_ne_zero_iff_separable.{u} {R : Type u} [Field R]
  [IsAddTorsionFree R] [DecidableEq R] [Hex.ExactDivLaws R]
  (f : Hex.DensePoly R) (hf : 0 < f.natDegree) :
  f.disc ≠ 0 ↔ (HexPolyMathlib.toPolynomial f).Separable
Hex.DensePoly.disc_ne_zero_iff_separable.{u}
  {R : Type u} [Field R]
  [IsAddTorsionFree R] [DecidableEq R]
  [Hex.ExactDivLaws R]
  (f : Hex.DensePoly R)
  (hf : 0 < f.natDegree) :
  f.disc ≠ 0 ↔
    (HexPolyMathlib.toPolynomial
        f).Separable

A positive-degree polynomial over a characteristic-zero field has nonzero executable discriminant exactly when it is separable.

The specialization contract retains the original formal degrees, so degree drops after substituting a parameter do not silently change the resultant convention:

theorem

Hex.DensePoly.eval_resultant.{u} {R : Type u} [CommRing R]
  [DecidableEq R] [Div R] [Hex.ExactDivLaws R]
  (f g : Hex.DensePoly (Hex.DensePoly R)) (a : R) :
  (f.resultant g).eval a =
    (f.specialize a).resultant (g.specialize a) f.natDegree g.natDegree
Hex.DensePoly.eval_resultant.{u}
  {R : Type u} [CommRing R]
  [DecidableEq R] [Div R]
  [Hex.ExactDivLaws R]
  (f g : Hex.DensePoly (Hex.DensePoly R))
  (a : R) :
  (f.resultant g).eval a =
    (f.specialize a).resultant
      (g.specialize a) f.natDegree
      g.natDegree

Specializing the coefficient variable after elimination agrees with the formal-degree Mathlib resultant of the specialized inputs.

Mathlib's resultant has the following proved root-product formula. Together with the executable correspondence, this identity underlies one-level field norms and the Trager collision bound:

theorem

Hex.DensePoly.resultant_eq_leadingCoeff_mul_prod_roots.{u} {K : Type u}
  [Field K] [IsAlgClosed K] (f g : Polynomial K) :
  f.resultant g =
    f.leadingCoeff ^ g.natDegree *
      (Multiset.map (fun x => Polynomial.eval x g) f.roots).prod
Hex.DensePoly.resultant_eq_leadingCoeff_mul_prod_roots.{u}
  {K : Type u} [Field K] [IsAlgClosed K]
  (f g : Polynomial K) :
  f.resultant g =
    f.leadingCoeff ^ g.natDegree *
      (Multiset.map
          (fun x => Polynomial.eval x g)
          f.roots).prod

The resultant as the leading-coefficient power times evaluation over all roots of the first polynomial, counted with multiplicity.

Its immediate consequence is the classical vanishing criterion, stated over the complex numbers for integer inputs:

theorem

Hex.DensePoly.resultant_eq_zero_iff_common_root (f g : Hex.DensePoly ℤ)
  (hf : f ≠ 0) :
  f.resultant g = 0 ↔
    ∃ z,
      (Polynomial.aeval z) (HexPolyMathlib.toPolynomial f) = 0 ∧
        (Polynomial.aeval z) (HexPolyMathlib.toPolynomial g) = 0
Hex.DensePoly.resultant_eq_zero_iff_common_root
  (f g : Hex.DensePoly ℤ) (hf : f ≠ 0) :
  f.resultant g = 0 ↔
    ∃ z,
      (Polynomial.aeval z)
            (HexPolyMathlib.toPolynomial
              f) =
          0 ∧
        (Polynomial.aeval z)
            (HexPolyMathlib.toPolynomial
              g) =
          0

If the first integer dense polynomial is nonzero, the executable resultant vanishes exactly when the two polynomials share a complex root.