The executable coefficientwise reduction Hex.ZPoly.modP agrees with
Mathlib's coefficient map from ℤ[X] to (ZMod p)[X] after transporting the
resulting FpPoly through the Berlekamp transport.
The Mathlib ZMod p-cast of the leading coefficient of a Hex.ZPoly agrees
with the executable ZMod64-valued leadingCoeffModP after transport along
ZMod64.toZMod. This is the integer-side companion to the modular modP
lemma: it lets a downstream caller chain the executable good-prime
hypothesis through to the Mathlib Polynomial.map natural-degree lemma.
The Mathlib ZMod p-cast of the leading coefficient of a Hex.ZPoly is
nonzero exactly when the executable leadingCoeffModP is. This packages the
direction needed by the integer-factor degree-preservation step in
checkIrreducibleCert_sound.
Reduction modulo p preserves natural degree when the executable
leadingCoeffModP data records a nonzero leading coefficient. This is the
_of_unit_lc_mod_p shape: the executable good-prime check supplies
the leadingCoeffModP ≠ 0 hypothesis, and natDegree is preserved along the
Mathlib Polynomial.map reduction.
Reduction-mod-p Gauss lemma over ℤ: a primitive integer polynomial whose
modular reduction is irreducible and whose leading coefficient is not killed
by the reduction is itself irreducible.
Hex.ZPoly-level transfer of irreducible_of_isPrimitive_of_irreducible_map_intCast_zmod.
Given a Hex.ZPoly square-free part whose Mathlib image is primitive, with a prime p
whose action via Int.castRingHom (ZMod p) does not kill the leading
coefficient, and with the reduction Mathlib-irreducible, the original polynomial is
Hex.ZPoly.Irreducible via the existing equivalence.
Small-mod singleton branch primitive-square-free-part irreducibility, stated at the executable
Hex.ZPoly level.
The branch-specific executable facts identify the relevant modular image as
Hex.ZPoly.modP p core; the coefficientwise commutation lemma rewrites its
Mathlib irreducibility into the Polynomial.map (Int.castRingHom (ZMod p))
hypothesis consumed by the primitive Gauss transfer above.
Variant of Hex_ZPoly_Irreducible_of_irreducible_modP for the
PrimeChoiceData surface used by the Berlekamp-Zassenhaus branches.
The executable prime-choice record stores the modular image as fModP; callers
provide the existing equality identifying it with Hex.ZPoly.modP p core.
Small-mod singleton branch irreducibility package for the selected primitive square-free part.
The branch hypotheses mirror the executable shape: the fast path
reassembles from the singleton primitive square-free part when the selected modular
factor list has size at most one. The mathematical irreducibility payload is
kept as an explicit PrimeChoiceData.fModP irreducibility hypothesis, so the
eventual Berlekamp singleton theorem can replace it directly.
The executable size-one gcd test is exactly Mathlib coprimality after
transport to Polynomial (ZMod p).
Small-mod singleton irreducibility composed without the explicit
hirr_fModP hypothesis.
Given a choosePrimeData? success witness and a singleton-bounded
modular-factor count, the executable factorsModP array packaged by
choosePrimeData?_factorsModP_berlekamp_form is the Berlekamp factor
output for the monic modular image; the irreducible_of_berlekampFactor_factors_length_le_one
no-split lemma then turns this into Mathlib irreducibility of the monic
modular image, which transfers along toMathlibPolynomial_scale to
Mathlib irreducibility of fModP and finally to integer-level
irreducibility of core.
The square-free precondition on the monic modular image is supplied
explicitly. irreducible_of_smallMod derives it from the selected good-prime
record.
Small-mod singleton irreducibility for a selected good-prime record, deriving
the Berlekamp square-free precondition for the monic modular image from the
selected prime's executable squareFreeModP check.
The Mathlib image over ZMod p of the monic modular reduction selected by a
successful choosePrimeData? run is squarefree.
The executable isGoodPrime check certifies squareFreeModP core p
(gcdIsUnit (gcd (modP core) (modP core)') = true);
gcd_monicModularImage_derivative_isUnit lifts this to the monic image's
coprimality with its derivative, which is exactly Polynomial.Separable over the
field ZMod p, hence Squarefree. This is the modular squarefreeness datum the
mod-p disjointness lemma modPFactorSubset_disjoint_of_not_associated needs but
modPSubsetPartitionHypotheses_of_choosePrimeData fills with trivial.
Identification of the executable Hex.ZPoly.Primitive predicate with Mathlib's
Polynomial.IsPrimitive on the transported polynomial.
If the integer-coefficient gcd of f is 1, then any integer r whose
constant polynomial C r divides toPolynomial f must divide every
coefficient of f, hence divides the executable content f = 1, hence
|r| = 1, hence r is a unit.
The product squareFreeCore * repeatedPart extracted from a nonzero
integer polynomial by Hex.normalizeForFactor is executably primitive.
The primitive square-free part extracted by normalizeForFactor is primitive
over Polynomial ℤ whenever the input integer polynomial is nonzero.
The proof uses the executable Hex.ZPoly.Primitive predicate
on squareFreeCore * repeatedPart (from
primitiveSquareFreeDecomposition_squareFreeCore_repeatedPart_primitive),
transports it to Polynomial ℤ via
toPolynomial_isPrimitive_of_zpoly_primitive, and drops to the square-free
factor via Mathlib's Polynomial.isPrimitive_of_dvd.
This discharges the hprim hypothesis required by
squareFreeCore_irreducible_of_small_mod_singleton.
The repeated part extracted by normalizeForFactor is primitive over
Polynomial ℤ whenever the input integer polynomial is nonzero.
This is the companion Gauss-descent input to
normalizeForFactor_squareFreeCore_toPolynomial_isPrimitive for the
structural divisibility theorem consumed by the exponent-extraction
successor.
The repeated part extracted by normalizeForFactor is already
normalize-fixed after transport to Polynomial ℤ.
This packages the executable nonnegative-leading-coefficient invariant in the form expected by UFD uniqueness arguments.
The executable formal derivative on Hex.DensePoly R agrees with Mathlib's
Polynomial.derivative under the HexPolyMathlib.toPolynomial transport, for
any commutative semiring with decidable equality.
The rational view of an integer polynomial through the executable
Hex.ZPoly.toRatPoly agrees with the integer-side toPolynomial
post-composed with Polynomial.map (Int.castRingHom ℚ). This is the
identity that lets the executable SquareFreeRat invariant be read as
a Mathlib statement about the rational image of toPolynomial f.
The executable Hex.ZPoly.SquareFreeRat invariant transports to
IsCoprime of the rational image of toPolynomial f with its formal
derivative. This is the field-side discharge of the squarefree
predicate: once the executable rational gcd is shown to be a unit (which
follows from (gcd …).size ≤ 1 together with f ≠ 0), the
gcd-associatedness lemma HexPolyMathlib.toPolynomial_gcd_associated
forces the Mathlib gcd to be a unit too, which is IsCoprime.
Gauss-style descent for squarefreeness: a primitive integer polynomial is squarefree iff its rational image is, and in particular the implication from rational to integer follows.
Given p : Polynomial ℤ primitive and Squarefree (p.map (Int.castRingHom ℚ)),
any square factor q² ∣ p lifts to (q.map …)² ∣ p.map …, forcing
q.map … to be a unit; the injective cast then pins q to a nonzero
constant C n, and primitivity of p plus C (n * n) ∣ p forces n * n
(hence n, hence q) to be a unit in ℤ[X].
The primitive square-free part extracted by normalizeForFactor is squarefree over
Polynomial ℤ whenever the input integer polynomial is nonzero.
The proof composes the rational-side squarefreeness obtained from the
executable Hex.ZPoly.SquareFreeRat invariant
(primitiveSquareFreeDecomposition_squareFreeCore,
HexPolyZ/Basic.lean:2997) via Separable.squarefree with the
Gauss-style descent
squarefree_of_isPrimitive_of_squarefree_map_intCast, using the
existing primitivity lemma
normalizeForFactor_squareFreeCore_toPolynomial_isPrimitive.
This lets liftedFactorSubsetPartition_outerBound_of_choosePrimeData
derive squarefreeness directly from f ≠ 0.
Identification of the executable isGoodPrime invariant with the Mathlib
Int.castRingHom (ZMod p)-cast leading-coefficient nonvanishing
required by the reduction-mod-p machinery.
The good-prime predicate carries leadingCoeffAdmissible, i.e. the
executable leadingCoeffModP is nonzero; the iff lemma
intCast_zmod_leadingCoeff_ne_zero_iff_leadingCoeffModP_ne_zero
translates that into the Mathlib cast form.
Variant of leadingCoeff_castRingHom_ne_zero_of_isGoodPrime specialised
to a choosePrimeData?-selected good prime.
Discharges the hlc_map_ne hypothesis required by
squareFreeCore_irreducible_of_small_mod_singleton when the executable
prime selection succeeds: the chosen prime's ZMod-cast leading
coefficient is nonzero because choosePrimeData?_isGoodPrime certifies
the isGoodPrime invariant.
Reverse identification from Mathlib's Polynomial.IsPrimitive on the transported
polynomial to the executable Hex.ZPoly.Primitive predicate.
Apply IsPrimitive at the constant polynomial C (content f) (which divides
toPolynomial f because content f divides every integer coefficient), to
conclude IsUnit (content f) in ℤ. Combined with the non-negativity of
Hex.ZPoly.content (it is Int.ofNat of DensePoly.contentNat), this forces
content f = 1.
The primitive square-free part extracted by normalizeForFactor is executably
primitive whenever the input integer polynomial is nonzero.
The proof transports
normalizeForFactor_squareFreeCore_toPolynomial_isPrimitive back to
Hex.ZPoly via zpoly_primitive_of_toPolynomial_isPrimitive.
For a polynomial p over a characteristic-zero field K, the executable gcd
gcd p p' is associated to divRadical p = p / radical p.
Mathlib already supplies the easy direction
divRadical p ∣ gcd p p' (via divRadical_dvd_self and
divRadical_dvd_derivative in Mathlib/RingTheory/Polynomial/Radical.lean).
The reverse direction gcd p p' ∣ divRadical p is the char-0 multiplicity
fact: for a prime q in K[X] and p = q^e * f coprime to q, in
char-0 the derivative p' has q-multiplicity exactly e - 1, so
gcd p p' has q-multiplicity min(e, e-1) = e - 1.
The proof goes by UniqueFactorizationMonoid.induction_on_coprime. The
prime-power case uses dvd_prime_pow to extract a candidate exponent and
discharges the saturating case by combining char-0 with separability
(PerfectField.separable_of_irreducible from PerfectField.ofCharZero).
The coprime case uses the GCDMonoid lemma dvd_gcd_mul_of_dvd_mul
applied twice to factor divisibility through component gcds, then chains
each component to the inductive hypothesis via IsCoprime.dvd_of_dvd_mul_right.