Interpret an executable integer polynomial as a Mathlib polynomial.
9.8. The Mathlib correspondence
Everything above is executable and Mathlib-free. HexPolyZMathlib is
the proof-facing companion: it identifies Hex.ZPoly with
Mathlib's Polynomial ℤ, transports the integer-polynomial operations
used by factorization, and proves the analytic bounds that justify the
executable estimates.
9.8.1. Conversion and ring operations
The two conversion functions preserve coefficients and are mutually inverse.
def
def
Rebuild an executable integer polynomial from a Mathlib polynomial.
theorem
HexPolyZMathlib.coeff_toPolynomial (p : Hex.ZPoly) (n : ℕ) : (HexPolyZMathlib.toPolynomial p).coeff n = Hex.DensePoly.coeff p nHexPolyZMathlib.coeff_toPolynomial (p : Hex.ZPoly) (n : ℕ) : (HexPolyZMathlib.toPolynomial p).coeff n = Hex.DensePoly.coeff p n
Coefficients of the embedded Mathlib polynomial agree with the executable coefficients.
theorem
HexPolyZMathlib.toPolynomial_ofPolynomial (p : Polynomial ℤ) : HexPolyZMathlib.toPolynomial (HexPolyZMathlib.ofPolynomial p) = pHexPolyZMathlib.toPolynomial_ofPolynomial (p : Polynomial ℤ) : HexPolyZMathlib.toPolynomial (HexPolyZMathlib.ofPolynomial p) = p
toPolynomial is a left inverse of ofPolynomial: embedding a rebuilt
polynomial recovers it.
theorem
ofPolynomial is a left inverse of toPolynomial: rebuilding an embedded
ZPoly recovers it.
They are bundled as a ring equivalence, so zero, one, constants, addition, multiplication, negation, and subtraction transport without changing their meaning.
def
The executable ZPoly representation is ring-equivalent to Mathlib
polynomials over ℤ.
theorem
toPolynomial sends the zero ZPoly to the zero polynomial.
theorem
toPolynomial sends the executable 1 to Mathlib's 1.
theorem
HexPolyZMathlib.toPolynomial_C (c : ℤ) : HexPolyZMathlib.toPolynomial (Hex.DensePoly.C c) = Polynomial.C cHexPolyZMathlib.toPolynomial_C (c : ℤ) : HexPolyZMathlib.toPolynomial (Hex.DensePoly.C c) = Polynomial.C c
toPolynomial sends the executable constant C c to Mathlib's Polynomial.C c.
theorem
toPolynomial is additive.
theorem
toPolynomial is multiplicative.
theorem
toPolynomial commutes with negation.
theorem
toPolynomial commutes with subtraction.
The example below illustrates the usual proof pattern. Convert to
Polynomial ℤ, use the simplification rules supplied by
HexPolyZMathlib, and convert back only if executable data is needed
again.
open HexPolyZMathlib
namespace HexPolyZChapterCorrespondence
example (f g : Hex.ZPoly) :
ofPolynomial (toPolynomial (f * g)) = f * g := f:ZPolyg:ZPoly⊢ ofPolynomial (toPolynomial (f * g)) = f * g
All goals completed! 🐙
example (f : Hex.ZPoly) (n : Nat) :
(toPolynomial f).coeff n = f.coeff n := f:ZPolyn:ℕ⊢ (toPolynomial f).coeff n = coeff f n
All goals completed! 🐙
end HexPolyZChapterCorrespondence
9.8.2. Integer-specific transports
HexPolyZMathlib also names the transports that do not follow from the
ring equivalence alone. The Mathlib-free unit predicate agrees with
IsUnit. Variable dilation becomes composition by C c * X.
The executable content and primitive-part decomposition agrees with
Mathlib's Gauss decomposition.
theorem
HexPolyZMathlib.isUnit_iff_toPolynomial_isUnit (f : Hex.ZPoly) : f.IsUnit ↔ IsUnit (HexPolyZMathlib.toPolynomial f)HexPolyZMathlib.isUnit_iff_toPolynomial_isUnit (f : Hex.ZPoly) : f.IsUnit ↔ IsUnit (HexPolyZMathlib.toPolynomial f)
The Mathlib-free ZPoly unit predicate agrees with Mathlib units after
transport to Polynomial ℤ.
theorem
HexPolyZMathlib.toPolynomial_dilate (c : ℤ) (g : Hex.ZPoly) : HexPolyZMathlib.toPolynomial (Hex.ZPoly.dilate c g) = (HexPolyZMathlib.toPolynomial g).comp (Polynomial.C c * Polynomial.X)HexPolyZMathlib.toPolynomial_dilate (c : ℤ) (g : Hex.ZPoly) : HexPolyZMathlib.toPolynomial (Hex.ZPoly.dilate c g) = (HexPolyZMathlib.toPolynomial g).comp (Polynomial.C c * Polynomial.X)
The executable variable-dilation X ↦ c · X corresponds to Mathlib
composition with C c * X.
theorem
HexPolyZMathlib.toPolynomial_content (f : Hex.ZPoly) : (HexPolyZMathlib.toPolynomial f).content = f.contentHexPolyZMathlib.toPolynomial_content (f : Hex.ZPoly) : (HexPolyZMathlib.toPolynomial f).content = f.content
The Mathlib content of the embedded polynomial agrees with the executable integer content. Both are the normalized (nonnegative) gcd of the coefficients, so this is the Gauss correspondence between the two content theories.
theorem
HexPolyZMathlib.toPolynomial_eq_C_content_mul_primitivePart (f : Hex.ZPoly) : HexPolyZMathlib.toPolynomial f = Polynomial.C f.content * HexPolyZMathlib.toPolynomial f.primitivePartHexPolyZMathlib.toPolynomial_eq_C_content_mul_primitivePart (f : Hex.ZPoly) : HexPolyZMathlib.toPolynomial f = Polynomial.C f.content * HexPolyZMathlib.toPolynomial f.primitivePart
Gauss content decomposition transported to Mathlib: the embedded polynomial is its content times the embedded primitive part.
theorem
HexPolyZMathlib.isPrimitive_toPolynomial_of_primitive (f : Hex.ZPoly) (hf : f.Primitive) : (HexPolyZMathlib.toPolynomial f).IsPrimitiveHexPolyZMathlib.isPrimitive_toPolynomial_of_primitive (f : Hex.ZPoly) (hf : f.Primitive) : (HexPolyZMathlib.toPolynomial f).IsPrimitive
A primitive executable polynomial embeds to a Mathlib-primitive polynomial.
Hex.ZPoly.modP reduces integer coefficients into executable
Hex.ZMod64 values. The coefficient theorem identifies them with
the corresponding values in Mathlib's ZMod type. It is the
rewrite rule used to prove the extensional map theorem. Divisibility
transports separately because Polynomial.map preserves
multiplication.
theorem
HexPolyZMathlib.coeff_toZMod_modP_eq_coeff_map_intCast (p : ℕ) [Hex.ZMod64.Bounds p] (f : Hex.ZPoly) (n : ℕ) : HexModArithMathlib.ZMod64.toZMod (Hex.DensePoly.coeff (Hex.ZPoly.modP p f) n) = (Polynomial.map (Int.castRingHom (ZMod p)) (HexPolyZMathlib.toPolynomial f)).coeff nHexPolyZMathlib.coeff_toZMod_modP_eq_coeff_map_intCast (p : ℕ) [Hex.ZMod64.Bounds p] (f : Hex.ZPoly) (n : ℕ) : HexModArithMathlib.ZMod64.toZMod (Hex.DensePoly.coeff (Hex.ZPoly.modP p f) n) = (Polynomial.map (Int.castRingHom (ZMod p)) (HexPolyZMathlib.toPolynomial f)).coeff n
The executable coefficientwise reduction Hex.ZPoly.modP agrees with
Mathlib's coefficient map from ℤ[X] to (ZMod p)[X], after transporting
the executable ZMod64 p coefficients through the ZMod64/ZMod equivalence.
theorem
HexPolyZMathlib.eq_map_intCast_of_coeff_eq_toZMod_modP (p : ℕ) [Hex.ZMod64.Bounds p] (f : Hex.ZPoly) {q : Polynomial (ZMod p)} (hq : ∀ (n : ℕ), q.coeff n = HexModArithMathlib.ZMod64.toZMod (Hex.DensePoly.coeff (Hex.ZPoly.modP p f) n)) : q = Polynomial.map (Int.castRingHom (ZMod p)) (HexPolyZMathlib.toPolynomial f)HexPolyZMathlib.eq_map_intCast_of_coeff_eq_toZMod_modP (p : ℕ) [Hex.ZMod64.Bounds p] (f : Hex.ZPoly) {q : Polynomial (ZMod p)} (hq : ∀ (n : ℕ), q.coeff n = HexModArithMathlib.ZMod64.toZMod (Hex.DensePoly.coeff (Hex.ZPoly.modP p f) n)) : q = Polynomial.map (Int.castRingHom (ZMod p)) (HexPolyZMathlib.toPolynomial f)
Extensional equality for any Mathlib polynomial over ZMod p whose
coefficients are supplied by the executable Hex.ZPoly.modP image.
Downstream finite-field polynomial transports can instantiate the coefficient
hypothesis with their own FpPoly coefficient lemma.
theorem
HexPolyZMathlib.dvd_modP_of_dvd (p : ℕ) {g f : Hex.ZPoly} (hgf : g ∣ f) : Polynomial.map (Int.castRingHom (ZMod p)) (HexPolyZMathlib.toPolynomial g) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (HexPolyZMathlib.toPolynomial f)HexPolyZMathlib.dvd_modP_of_dvd (p : ℕ) {g f : Hex.ZPoly} (hgf : g ∣ f) : Polynomial.map (Int.castRingHom (ZMod p)) (HexPolyZMathlib.toPolynomial g) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (HexPolyZMathlib.toPolynomial f)
Divisibility of executable integer polynomials transports to divisibility of
their Mathlib reductions modulo p.
9.8.3. Correctness theorems and the proof boundary
The executable library computes a natural-number squared coefficient
norm and a conservative integer bound. The companion identifies that
norm with the square of the real l2norm, identifies the executable
binomial coefficient with Nat.choose, and then applies Mathlib's
Mahler-measure theory to prove Mignotte's coefficient bound for every
factor of a nonzero integer polynomial.
def
The Euclidean norm of the coefficient vector of an integer polynomial.
theorem
The transported Mathlib coefficient-vector norm squared is exactly the executable squared coefficient norm; the executable range only pads Mathlib's finite support with zero coefficients.
theorem
The executable Mignotte-bound binomial coefficient agrees with Mathlib's
Nat.choose.
theorem
HexPolyZMathlib.mignotte_bound (f g : Polynomial ℤ) (hf : f ≠ 0) (hg : g ∣ f) (j : ℕ) : ↑(g.coeff j).natAbs ≤ ↑(g.natDegree.choose j) * HexPolyZMathlib.l2norm fHexPolyZMathlib.mignotte_bound (f g : Polynomial ℤ) (hf : f ≠ 0) (hg : g ∣ f) (j : ℕ) : ↑(g.coeff j).natAbs ≤ ↑(g.natDegree.choose j) * HexPolyZMathlib.l2norm f
Mignotte's coefficient bound for integer polynomial factors, obtained by combining Mathlib's Mahler-measure coefficient estimate with Landau's inequality.
HexPolyZMathlib also relates the executable rational squarefreeness
test to Mathlib's Squarefree predicate after casting to
Polynomial ℚ. Its discriminant, Hadamard, Robinson-form, and
Mahler-separation theorems remain entirely on the Mathlib side for
downstream certified factorization and root isolation proofs.
theorem
HexPolyZMathlib.squareFreeRat_iff (f : Hex.ZPoly) (hf : f ≠ 0) : f.SquareFreeRat ↔ Squarefree (HexPolyZMathlib.toPolyℚ f)HexPolyZMathlib.squareFreeRat_iff (f : Hex.ZPoly) (hf : f ≠ 0) : f.SquareFreeRat ↔ Squarefree (HexPolyZMathlib.toPolyℚ f)
For a nonzero executable integer polynomial, the executable rational-gcd test is equivalent to squarefreeness of its rational cast.
theorem
HexPolyZMathlib.one_le_mahlerDist (p : Polynomial ℤ) (hp : p ≠ 0) {z₁ z₂ : ℂ} (hr₁ : (Polynomial.map (Int.castRingHom ℂ) p).IsRoot z₁) (hr₂ : (Polynomial.map (Int.castRingHom ℂ) p).IsRoot z₂) (hne : z₁ ≠ z₂) : 1 ≤ √↑p.natDegree ^ (p.natDegree + 2) * (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure ^ (p.natDegree - 1) * ‖z₁ - z₂‖HexPolyZMathlib.one_le_mahlerDist (p : Polynomial ℤ) (hp : p ≠ 0) {z₁ z₂ : ℂ} (hr₁ : (Polynomial.map (Int.castRingHom ℂ) p).IsRoot z₁) (hr₂ : (Polynomial.map (Int.castRingHom ℂ) p).IsRoot z₂) (hne : z₁ ≠ z₂) : 1 ≤ √↑p.natDegree ^ (p.natDegree + 2) * (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure ^ (p.natDegree - 1) * ‖z₁ - z₂‖
Mahler separation for arbitrary nonzero integral polynomials. Repeated factors do not affect the set of roots: applying the separable theorem to the integral radical gives the same two roots, no larger degree, and no larger Mahler measure.
Thus callers use Hex.ZPoly and its natural-number bounds when
they need computation. They import HexPolyZMathlib only when a proof
must interpret those results as Mathlib polynomials or invoke
noncomputable algebraic and analytic theory. No Mathlib dependency
flows back into HexPolyZ.