monicModPImage is the identity on the mod-p reduction of a monic
integer polynomial, since the leading coefficient 1 reduces to 1 and
(1 : ZMod64 p)⁻¹ = 1.
A modular support representing an integer factor also represents that
factor's direct-coordinate monicTarget at any positive coprime precision.
Forward Hensel-lift transport for the canonical lifted subset: a monic
integer factor of core that is represented modulo primeData.p by a
modular-factor subset S is represented modulo primeData.p ^ B on the
integer side by the corresponding canonical lifted subset
liftedSubsetOfModPSubset primeData d hsize S.
The proof packages the subset/complement product modulo p ^ B
(henselLiftData_liftedFactorProduct_subset_complement_congr_core) and the
subset/complement coprimality modulo p
(henselLiftData_liftedSubset_complement_isCoprime_mod_p) into the
hypothesis list of HexHenselMathlib.hensel_unique, alongside the integer
factorization core = factor * q derived from factor ∣ core and the
mod-p subset representation hypothesis. Converting the resulting Mathlib
Polynomial.map equality back to the executable
Hex.ZPoly.reduceModPow form via
HexHenselMathlib.zpoly_congr_of_toPolynomial_map_eq and
Hex.ZPoly.reduceModPow_eq_of_congr discharges
RepresentsIntegerFactorAtLift.
This supplies the forward represents_lifted_of_modP field of
HenselSubsetLiftHypotheses; its hypotheses are the boundary facts provided
by Hex.choosePrimeData and Hex.henselLiftData.
Subset-level Hensel uniqueness in additive congruence form.
This is the main proof behind the recovered-coordinate
henselLiftData_represents_lifted_of_modP: if a selected modular subset S
represents a monic integer factor factor modulo p, and factor * cofactor
is a second factorisation of the same monic Hensel target modulo p ^ B, then
the canonical lifted subset product is congruent to factor modulo p ^ B.
The statement deliberately returns only the coefficientwise congruence. This
fits non-recovered coordinates such as the BHKS monicTarget M1 target, where
the product comparison is a modular target-coordinate assertion rather than an
integer equality target = factor * cofactor.
M1 (monicTarget-coordinate) subset Hensel uniqueness for directLiftData.
If the modular subset S represents the monicTarget coordinate of an integer
factor, and that coordinate participates in a modular factorisation of
monicTarget core p k, then the canonical selected product in
directLiftData core B primeData is congruent to monicTarget factor p k modulo
the Hensel modulus. The modular product decomposition is an explicit premise:
it is the scale-coordinate M1 fact to be supplied by callers, not something
derived from the older dilation-coordinate recovery carrier.
Centred-lift preserves monicness once the modulus is at least two.
The leading coefficient 1 of a monic input survives the centred-reduction
(centeredModNat 1 m = 1 for m ≥ 2) and DensePoly.ofCoeffs does not trim
it, so the output preserves both size and leading coefficient.
Array.polyProduct of an array all of whose entries are monic is monic.
The base case is Monic 1 (zpoly_monic_one); the inductive step chains
zpoly_monic_mul through each entry along the foldl accumulator.
A successful bhksIndicatorCandidate? call yields, under monic polynomial and
monic-selected-factor hypotheses, the canonical modular product equality
reduceModPow raw p k = reduceModPow candidate p k.
This is the per-candidate modular-product fact needed to derive the
RepresentsIntegerFactorAtLift certificate from a successful candidate path
and uses:
the centred-lift round-trip identity
centeredLiftPoly_reduceModPow_eq,monic_centeredLiftPoly_of_monicto push monicness through the centred lift,zpoly_primitive_of_monic+primitivePart_eq_self_of_primitiveto collapsenormalizeCandidateFactorto identity on monic input,zpoly_normalize_factor_sign_of_monicto collapsenormalizeFactorSignto identity on monic input.
The Mathlib-transported natDegree of the executable recombination candidate
over a lifted-factor subset equals the sum of the Mathlib-transported
natDegrees of the selected lifted factors.
Under the modulus condition 2 ≤ d.p ^ d.k and monicness of every lifted
factor, the candidate's centeredLiftPoly/primitivePart/normalizeFactorSign
chain collapses to a single monic polynomial whose stored size is the same as
the underlying lifted-factor product, so its Mathlib-side natDegree is the
sum over the subset.
This is the candidate-side ingredient of the reverse-coverage degree-counting
argument in the representedFactor_dvd_recombinationCandidate_of_subset
divisibility theorem.
The Mathlib-transported natDegree of a represented integer factor equals the
sum of the Mathlib-transported natDegrees of the lifted factors in the
representing subset.
On a monic polynomial, the partition pins the represented factor to its executable
recombination candidate (LiftedFactorSubsetPartition.recombinationCandidate_eq),
after which natDegree_toPolynomial_recombinationCandidate_eq_sum reads off the
degree sum. This uses the sound partition equality rather than passing
RepresentsIntegerFactorAtLift to the old scaled-product recovery lemmas.
Centred-lift preserves a strictly positive leading coefficient that lies inside the Mignotte half-window.
Abstract-bound variant of
natDegree_toPolynomial_scaledRecombinationCandidate_eq_sum: takes
B' : Nat, hcore_lc_le : (lc core).natAbs ≤ B', and
hprecision : 2 * B' < d.p ^ d.k in place of the input-shape
defaultFactorCoeffBound core precision constraint.
The single precision caller in the proof body is
size_centeredLiftPoly_eq_of_pos_leadingCoeff_bound, which requires a
leading-coefficient bound on scaledLiftedFactorProduct core d T. That
leading coefficient is lc core, so the hypothesis-supplied
hcore_lc_le discharges the precondition directly.
Follows the (B', hcore_lc_le, hprecision) parameter ordering
established by representsIntegerFactorAtLift_primitive_of_bound,
natDegree_toPolynomial_eq_sum_of_represents_of_primitive_pos_lc_core_of_bound,
and zpoly_primitive_scaledRecombinationCandidate_of_bound.
The Mathlib-transported natDegree of the scaled recombination candidate
over a lifted-factor subset equals the sum of the Mathlib-transported
natDegrees of the selected lifted factors, given primitive + positive-leading
core and the Mignotte precision bound.
The candidate goes through centeredLiftPoly ∘ primitivePart ∘ normalizeFactorSign
on top of scaledLiftedFactorProduct = scale (lc core) (liftedFactorProduct).
Each step preserves stored size: scaling by the nonzero leading coefficient,
centred-lift under the positive-leading bound, primitive part on a nonzero
input, and sign normalisation. Combined with lp.size = ∑ + 1 for the monic
lifted-factor product, the candidate's natDegree decomposes as a sum.
Thin wrapper over
natDegree_toPolynomial_scaledRecombinationCandidate_eq_sum_of_bound that
instantiates B' := Hex.ZPoly.defaultFactorCoeffBound core and discharges
hcore_lc_le via defaultFactorCoeffBound_valid core hcore_ne core hcore_dvd_self at index core.size - 1, converted to the leading
coefficient via leadingCoeff_eq_coeff_last.
Companion scaled variant of natDegree_toPolynomial_recombinationCandidate_eq_sum.
Consumed by the scaled cover-at-min chain for the primitive recursive
recombination coverage proof.
The Mathlib-transported natDegree of the corrected recovered candidate
equals the sum of the selected lifted-factor degrees. The selected product is
centred while monic, then variable-dilated by a nonzero leading coefficient;
both operations preserve the stored degree before primitive/sign
normalisation.
Abstract-bound wrapper for
natDegree_toPolynomial_liftedRecoveryCandidate_eq_sum. The bound and
precision hypotheses are used only to derive the modulus lower bound from the
positive leading coefficient.
Abstract-bound variant of
natDegree_toPolynomial_eq_sum_of_represents_of_primitive_pos_lc_core:
takes B' : Nat, hvalid : ∀ i, (factor.coeff i).natAbs ≤ B',
hcore_lc_le : (lc core).natAbs ≤ B', and
hprecision : 2 * B' < d.p ^ d.k in place of the input-shape
defaultFactorCoeffBound core precision constraint.
The unscaled _hrec_scaled step from the existing proof is dropped
entirely; its result was never consumed; and the centred-lift
recovery call is handled through
centeredLiftPoly_scaledLiftedFactorProduct_eq_factor_of_recovery_of_bound
in place of the input-shape recovery. Both changes make this sibling
independent of scaledRecombinationCandidate_eq_factor_of_recovery
and hence of the scaled recovery-candidate _of_bound chain.
Note: this sibling needs hcore_lc_le in addition to hvalid
because the size-preservation step
size_centeredLiftPoly_eq_of_pos_leadingCoeff_bound consumes a
leading-coefficient bound on scaledLiftedFactorProduct core d S,
whose leading coefficient is lc core. Without a B'-shape bound
on lc core itself, the abstract-precision hypothesis cannot
discharge that lemma's separation requirement. The existing
input-shape wrapper supplies this from
defaultFactorCoeffBound_valid core hcore_ne core hcore_dvd_self.
Primitive + positive-leading-coefficient polynomial variant of
natDegree_toPolynomial_eq_sum_of_represents.
For primitive non-monic core, the represented factor's natDegree equals the
sum of natDegrees of the selected lifted factors. The proof uses the
scaled recovery identity scaledRecombinationCandidate core d S = factor
and the size identities
factor.size = (scaledLiftedFactorProduct core d S).size = (liftedFactorProduct d S).size. Scaling by C (lc core) and the centred lift
both preserve stored size under the Mignotte half-window bound on lc core,
so the sum decomposition natDegree_prod_of_monic over liftedFactorProduct
applies unchanged. The hcore_primitive and hfactor_irr hypotheses are
threaded for API uniformity with the monic variant but are not used by the
proof; the natDegree extraction depends only on the leading-coefficient bound
and the primitive/sign-normalised facts on factor.
This is a thin wrapper over
natDegree_toPolynomial_eq_sum_of_represents_of_primitive_pos_lc_core_of_bound
that instantiates B' := Hex.ZPoly.defaultFactorCoeffBound core and discharges
hvalid via defaultFactorCoeffBound_valid core hcore_ne factor hdvd and the
leading-coefficient bound via
defaultFactorCoeffBound_valid core hcore_ne core hcore_dvd_self.
Converse to toPolynomial_ne_zero_and_not_isUnit_of_shouldRecord: if the
transported polynomial is non-zero and a non-unit, then the executable
shouldRecordPolynomialFactor check passes. Used to package executable
witnesses for one recombination split from Mathlib-side irreducibility.
An irreducible (after transport) Hex.ZPoly value passes the executable
shouldRecordPolynomialFactor check. Combines the previous lemma with
Irreducible's structural projections.
One-step exactQuotient? discharge for a recombination split: when the
candidate equals an integer divisor of core and is monic of positive degree,
the executable exact-division check returns some of the proof-side cofactor.
Scaled-candidate counterpart of exactQuotient?_recombinationCandidate_eq_some_of_eq_factor.
When the scaled candidate equals a monic integer divisor of target of
positive degree, the executable exact-division check on target returns
some of the proof-side cofactor.
This connects the recovery identity
scaledRecombinationCandidate_eq_factor_of_recovery to the exact-division
check in Hex.scaledRecombinationSearchModAux.
Non-monic counterpart of
exactQuotient?_scaledRecombinationCandidate_eq_some_of_eq_factor.
When the scaled candidate equals an integer divisor of target with positive
leading coefficient and positive degree, the executable exact-division check
on target returns some of the proof-side cofactor.
Drops Monic factor in favour of 0 < lc factor, handling through
exactQuotient?_eq_some_of_pos_lc_pos_degree_mul_eq instead of the
monic-only exactQuotient?_eq_some_of_mul_eq_monic_of_pos_degree. Consumed
by the primitive recursive coverage proof together with the recovery identity
scaledRecombinationCandidate_eq_factor_of_recovery and the primitive,
positive-leading bound from
representsIntegerFactorAtLift_primitive.
A Hex.ZPoly factor that passes the executable shouldRecordPolynomialFactor
check is non-zero and not a unit after transport to Polynomial ℤ. The
executable check rejects 0, 1, and -1, which are exactly the zero
and unit constants on the Mathlib side.