Composed convenience wrapper: combines
Hex.ZPoly.QuadraticMultifactorLiftInvariant_of_choosePrimeData with
henselLiftData_liftedFactor_injective so that a Mathlib-side caller can
discharge Function.Injective (liftedFactor (henselLiftData core B primeData))
from the choosePrimeData boundary facts plus factorsModP.toList.Nodup,
without having to construct the internal QuadraticMultifactorLiftInvariant
themselves.
Consumed by
recombinationSearchModAux_factor_associated
(via LiftedFactorListMatches.nodup_of_injOn).
The factorsModP.toList.Nodup hypothesis is the load-bearing ingredient;
discharge from the choosePrimeData? facts is provided by
factorsModP_nodup_of_factorsModPBerlekampForm above (combined with
Hex.choosePrimeData?_factorsModP_berlekamp_form). The companion monicness
umbrella henselLiftData_liftedFactor_monic_of_choosePrimeData lives one
theorem above.
Abstract-invariant umbrella for positive natural degree of each lifted factor
produced by Hex.henselLiftData.
Mirrors henselLiftData_liftedFactor_monic and _injective: takes the
recursive QuadraticMultifactorLiftInvariant package together with the
per-output mod-p product congruence and a per-factor natural-degree
positivity premise on the lift of each input factorsModP entry, and
concludes that every lifted factor's transported Mathlib polynomial has
positive natural degree.
The proof uses Hex.ZPoly.multifactorLiftQuadratic_each_congr_mod_base
to identify each lifted factor's mod-p reduction with the corresponding
modular factor (after FpPoly.liftToZ), then transports through the
toMathlibPolynomial/Polynomial.map map. Both the lifted factor and
its modular pre-image are monic, so reduction modulo p preserves natural
degree (their Polynomial.map (Int.castRingHom (ZMod p)) images have the
same natural degree as the unmapped polynomials), and the modular images
agree by congruence.
This is the natDegree-positivity discharge consumed by the outer-bound
slow-path wrapper
factor_exhaustive_branch_entry_core_zpolyIrreducible_of_henselSubsetCorrespondence
(see line 7590 below).
Composed convenience wrapper: combines
Hex.ZPoly.QuadraticMultifactorLiftInvariant_of_choosePrimeData with
henselLiftData_liftedFactor_natDegree_pos so that a Mathlib-side caller
can discharge positive natural degree of every lifted factor from the
choosePrimeData boundary facts plus per-modular-factor natural-degree
positivity.
The per-modular-factor natural-degree positivity premise mirrors the
hfactorsModP_nodup premise on the injectivity umbrella: it is
exposed as an explicit hypothesis here because discharging it from
choosePrimeData invariants requires composing with factorsModPBerlekampForm
and the underlying Berlekamp factor-degree positivity.
Monic integer polynomials are nonzero.
Identify liftedFactorProduct d S to a Finset.prod over S after transport to
Polynomial ℤ. The executable foldl form unfolds through toPolynomial_foldl_mul
and the resulting List.prod is then identified with the Mathlib Finset.prod
via Finset.prod_map_toList.
This is the algebra-to-Finset.prod lemma needed by the disjoint-union splitting
lemma liftedFactorProduct_eq_mul_sdiff_of_subset.
Product-level base-modulus preservation for the lifted factors selected by a modular-factor subset.
After transporting S through liftedSubsetOfModPSubset, the product of the
corresponding Hensel-lifted factors is congruent modulo primeData.p to the
canonical integer lift of the original modular subset product.
Subset/complement coprimality of Hensel-lifted factor products modulo
primeData.p.
After mapping both products into Polynomial (ZMod primeData.p), the
selected lifted-factor subset's product and the complementary subset's
product are coprime: each lifted product reduces (via
henselLiftData_liftedSubset_product_congr_mod_base and
Hex.FpPoly.modP_liftToZ) to the corresponding modPFactor subset
product, and the modPFactor entries are pairwise distinct monic
irreducibles in Polynomial (ZMod primeData.p), so any subset and its
complement are coprime.
This is the IsCoprime input over (ZMod primeData.p)[X] consumed by
HexHenselMathlib.hensel_unique when applied to the subset/complement
pair of Hensel-lifted factor products.
Multiplicative splitting for liftedFactorProduct along the disjoint
decomposition T = S ⊔ (T \ S) when S ⊆ T.
This is the executable analogue of Finset.prod_sdiff for the foldl product
over LiftedFactorSubset d. Proved by transporting to Polynomial ℤ via
toPolynomial_liftedFactorProduct and applying Finset.prod_sdiff there,
then inverting through HexPolyZMathlib.equiv.injective.
Multiplicative splitting for liftedFactorProduct along a disjoint union.
Specialisation of liftedFactorProduct_eq_mul_sdiff_of_subset to the case where
T = S ∪ U with S and U disjoint, so T \ S = U and the product factors
as liftedFactorProduct d (S ∪ U) = liftedFactorProduct d S * liftedFactorProduct d U.
The full lifted-factor product over Finset.univ collapses to the executable
Array.polyProduct of the raw lifted-factor array.
The proof uses HexPolyZMathlib.equiv.injective: under the
toPolynomial map, both sides expand to the same finite product over
Fin d.liftedFactors.size, using toPolynomial_liftedFactorProduct,
polyProduct_toPolynomial, and Finset.prod_univ_fun_getElem modulo the
Array.length_toList size identification.
This structural identification feeds the multifactor-lift product equality into subset-based recombination reasoning.
Under the recursive quadratic multifactor lift invariant, the product of all
Hensel-lifted local factors is congruent to core modulo primeData.p ^ B.
This is the umbrella wrapper combining
liftedFactorProduct_univ_eq_polyProduct_liftedFactors with
Hex.ZPoly.multifactorLiftQuadratic_spec so downstream subset-recombination
proofs can split the full product through
liftedFactorProduct_eq_mul_sdiff_of_subset.
The lifted-factor product over a subset times the lifted-factor product over
its complement (within Finset.univ) is congruent to core modulo
primeData.p ^ B, under the recursive quadratic multifactor lift invariant.
This packages the mod-p^k factorization input required by Hensel
uniqueness callers (HexHenselMathlib.hensel_unique): the subset product
plays the role of g and the complement product plays the role of h in
g * h ≡ core (mod p^k). The proof combines the full-product congruence
(henselLiftData_liftedFactorProduct_univ_congr_core) with the multiplicative
splitting liftedFactorProduct_eq_mul_sdiff_of_subset.
Multiplicative closure of the recovered/monic-coordinate representation carrier
RecoveredAtLift along a disjoint decomposition S ∪ T. If S recovers the
integer factor f and T (disjoint from S) recovers g, then S ∪ T
recovers f * g.
This holds for an arbitrary square-free part: the carrier separates the mod-p^k
congruence (on
the unscaled liftedFactorProduct) from the dilation by leadingCoeff core, so
no monicity hypothesis is needed. The witness monic coordinate is the product of
the two witnesses; the congr field combines
liftedFactorProduct_union_of_disjoint with Hex.ZPoly.congr_mul, and the
dilate_eq field combines HexPolyZMathlib.dilate_mul (dilation is
multiplicative) with Hex.ZPoly.primitivePart_mul (Gauss's lemma).
The monic_dvd field is not closed under the helper unconditionally: the
two component divisibilities hf.monicFactor ∣ (toMonic core).monic and
hg.monicFactor ∣ (toMonic core).monic do not give
hf.monicFactor * hg.monicFactor ∣ (toMonic core).monic without coprimality of
the two coordinates. The product divisibility is therefore taken as an explicit
premise hmul_dvd, supplied by the squarefree-lift context where it genuinely
holds.
Equations
- HexBerlekampZassenhausMathlib.RecoveredAtLift.mul hdisj hf hg hmul_dvd = { monicFactor := hf.monicFactor * hg.monicFactor, congr := ⋯, dilate_eq := ⋯, monic_dvd := hmul_dvd }
Instances For
Monic-product closure for liftedFactorProduct: when every selected lifted
factor is monic, the executable foldl product over the subset is monic too.
The induction unfolds Finset.toList and chains zpoly_monic_mul through each
* step starting from Monic (1 : ZPoly).
Monicity of the Hensel-lifted subset product under the quadratic multifactor lift invariant.
Each Hensel-lifted local factor is monic
(henselLiftData_liftedFactor_monic), and the foldl product of monic factors
is monic (liftedFactorProduct_monic), so any selected subset product is
monic. This is the monicity input required by
HexHenselMathlib.hensel_unique for the selected factor.