HexPolyZMathlib.PolynomialEquivalence

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.

source

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)) (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.

source

theorem HexPolyZMathlib.natDegree_map_intCast_zmod_eq_of_leadingCoeff_ne_zero (p : ℕ) (g : Hex.ZPoly) (hlc : (Int.castRingHom (ZMod p)) (toPolynomial g).leadingCoeff ≠ 0) :

(Polynomial.map (Int.castRingHom (ZMod p)) (toPolynomial g)).natDegree = (toPolynomial g).natDegree

Reduction modulo p preserves natural degree when the leading coefficient survives the map to ZMod p.

source

theorem HexPolyZMathlib.dvd_modP_of_dvd (p : ℕ) {g f : Hex.ZPoly} (hgf : g ∣ f) :

Polynomial.map (Int.castRingHom (ZMod p)) (toPolynomial g) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (toPolynomial f)

Divisibility of executable integer polynomials transports to divisibility of their Mathlib reductions modulo p.

source

theorem HexPolyZMathlib.toZMod_ZMod64_ofNat_intModNat_eq_intCast (p : ℕ) [Hex.ZMod64.Bounds p] (z : ℤ) :

HexModArithMathlib.ZMod64.toZMod (Hex.ZMod64.ofNat p (Hex.ZPoly.intModNat z p)) = ↑z

Integer-to-ZMod p identity underlying modP: pushing an integer through intModNat/ZMod64.ofNat and then to Mathlib's ZMod p via toZMod agrees with the direct integer cast.

source

@[simp]

theorem HexPolyZMathlib.toPolynomial_dilate (c : ℤ) (g : Hex.ZPoly) :

toPolynomial (Hex.ZPoly.dilate c g) = (toPolynomial g).comp (Polynomial.C c * Polynomial.X)

The executable variable-dilation X ↦ c · X corresponds to Mathlib composition with C c * X.

source

theorem HexPolyZMathlib.dilate_mul (c : ℤ) (g h : Hex.ZPoly) :

Hex.ZPoly.dilate c (g * h) = Hex.ZPoly.dilate c g * Hex.ZPoly.dilate c h

Variable dilation is multiplicative: substituting X ↦ c · X is a ring homomorphism, so it distributes over products.

source

theorem HexPolyZMathlib.natDegree_toPolynomial_dilate (c : ℤ) (hc : c ≠ 0) (g : Hex.ZPoly) :

(toPolynomial (Hex.ZPoly.dilate c g)).natDegree = (toPolynomial g).natDegree

For a nonzero dilation factor, variable dilation preserves natural degree: C c * X has degree 1 with a unit leading coefficient over the integers.

source

theorem HexPolyZMathlib.dvd_of_comp_unit_mul_X {R : Type u_1} [CommRing R] {u : R} (hu : IsUnit u) {a b : Polynomial R} (h : a.comp (Polynomial.C u * Polynomial.X) ∣ b.comp (Polynomial.C u * Polynomial.X)) :

a ∣ b

Substitution X ↦ u · X by a unit u reflects divisibility: if the dilated polynomials divide, so do the originals. The substitution is a ring automorphism of R[X] with inverse X ↦ u⁻¹ · X, so applying that inverse hom to the hypothesis (via map_dvd) recovers a ∣ b. This is the substitution engine the lift-stage recovery chain uses to descend a divisibility through X ↦ lc · X, where lc is a unit because the prime does not divide the leading coefficient.

source

theorem HexPolyZMathlib.comp_unit_mul_X_dvd_iff {R : Type u_1} [CommRing R] {u : R} (hu : IsUnit u) {a b : Polynomial R} :

a.comp (Polynomial.C u * Polynomial.X) ∣ b.comp (Polynomial.C u * Polynomial.X) ↔ a ∣ b

Divisibility is invariant under substitution X ↦ u · X by a unit: the dilated polynomials divide iff the originals do. The forward direction is map_dvd of the composition ring hom (no unit needed); the reverse is dvd_of_comp_unit_mul_X.

source

theorem HexPolyZMathlib.isCoprime_comp_unit_mul_X_iff {R : Type u_1} [CommSemiring R] {u : R} (hu : IsUnit u) {a b : Polynomial R} :

IsCoprime (a.comp (Polynomial.C u * Polynomial.X)) (b.comp (Polynomial.C u * Polynomial.X)) ↔ IsCoprime a b

Coprimality is invariant under the invertible variable substitution X ↦ u * X. This is the Bézout counterpart of comp_unit_mul_X_dvd_iff.

source

theorem HexPolyZMathlib.toPolynomial_content (f : Hex.ZPoly) :

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

source

theorem HexPolyZMathlib.toPolynomial_eq_C_content_mul_primitivePart (f : Hex.ZPoly) :

toPolynomial f = Polynomial.C f.content * toPolynomial f.primitivePart

Gauss content decomposition transported to Mathlib: the embedded polynomial is its content times the embedded primitive part.

source

theorem HexPolyZMathlib.isPrimitive_toPolynomial_of_primitive (f : Hex.ZPoly) (hf : f.Primitive) :

(toPolynomial f).IsPrimitive

A primitive executable polynomial embeds to a Mathlib-primitive polynomial.

source

theorem HexPolyZMathlib.content_ne_zero (f : Hex.ZPoly) (hf : f ≠ 0) :

f.content ≠ 0

A nonzero executable polynomial has nonzero content.

source

theorem HexPolyZMathlib.dilate_recovery (core g h : Hex.ZPoly) (lc : ℤ) (d : ℕ) (hlc0 : lc ≠ 0) (hcore0 : core ≠ 0) (hkey : Hex.DensePoly.C (lc ^ (d - 1)) * core = Hex.ZPoly.dilate lc g * Hex.ZPoly.dilate lc h) :

toPolynomial (Hex.ZPoly.dilate lc g).primitivePart ∣ toPolynomial core ∧ (Hex.ZPoly.dilate lc g).primitivePart.Primitive ∧ (toPolynomial (Hex.ZPoly.dilate lc g).primitivePart).natDegree = (toPolynomial g).natDegree

Packaged recombination recovery. Given the keystone product identity C (lc^(d-1)) * core = dilate lc g * dilate lc h (the executable keystone dilate_transformedCore combined with dilate_mul), with lc ≠ 0 and a nonzero core, the primitive part of dilate lc g divides core, is primitive, and has the same degree as g. This is the inverse-factor correspondence the recombination recovery proof consumes.