Constant scaling preserves coefficientwise congruence modulo m:
f ≡ g (mod m) → c·f ≡ c·g (mod m).
Scalar multiplications multiply through a polynomial product.
Scalar multiplications compose.
Congruent integer scalars produce coefficientwise-congruent scalings.
The BHKS monicTarget is, coefficientwise modulo p^k, the rescaling of
core by the modular inverse of its leading coefficient:
monicTarget core p k ≡ core · ℓf⁻¹ (mod p^k). Immediate from
monicTarget = reduceModPow (scale ℓf⁻¹ core) p k.
Multiplication of direct-coordinate monic targets follows multiplication of their integer polynomials modulo the Hensel modulus.
The BHKS mod-correspondence: rescaling the monicTarget by ℓf = leadingCoeff core
recovers core modulo p^k, i.e. ℓf · monicTarget core p k ≡ core (mod p^k),
provided core's leading coefficient is coprime to p^k (the good-prime
condition). This is what lets the lifted monic factors of monicTarget recover
integer factors of core directly in core's own coordinate.
The original-coordinate scaled-product congruence: given the M1 lift congruence
∏ liftedFactors ≡ monicTarget core p k (mod p^k) for a selected subset S,
the ℓf-scaled lifted product is congruent to core itself modulo p^k:
scaledLiftedFactorProduct core d S ≡ core (mod p^k). This is the precise
hypothesis the existing Mignotte recovery
(centeredLift_scaledLiftedFactorProduct_eq_of_mignottePrecision) consumes,
delivered in core's own coordinate.
A subset product congruent to a factor's direct monic target recovers that factor after scaling by its leading coefficient.
Scale a factor-coordinate congruence through the leading-coefficient factorization of the original polynomial.
Compose direct-target recovery with the original polynomial's leading-coefficient factorization.
M1 (monicTarget-coordinate) recovery witness, the van Hoeij analogue of
RecoveredAtLift.
The selected lifted product represents a monic-coordinate factor monicFactor
modulo p^k; the integer factor is recovered by scaling that monic factor by
ℓf = leadingCoeff core and taking the primitive part of its centred lift; no
dilate, because the monicTarget coordinate already is core's coordinate
(monicTarget ≡ core·ℓf⁻¹). Accordingly monic_dvd pins monicFactor to a
divisor of monicTarget core p k rather than (toMonic core).monic.
Stated standalone (a fresh carrier with its own recovery lemma candidate_eq)
so it lands green without rerouting any existing RecoveredAtLift (M2) consumer.
- monicFactor : Hex.ZPoly
The direct-coordinate factor represented by the selected lifted factors.
The selected lifted product agrees with that factor modulo the lift modulus.
- recovered_eq : (Hex.centeredLiftPoly (Hex.ZPoly.reduceModPow (Hex.DensePoly.scale (Hex.DensePoly.leadingCoeff core) self.monicFactor) d.p d.k) (d.p ^ d.k)).primitivePart = factor
Scaling and centred lifting recover the original integer factor.
The direct-coordinate factor divides the polynomial lifted by Hensel's method.
Instances For
Recovery formula in core's own coordinate: an M1 recovery witness recovers
its integer factor as the primitive part of the centred lift of the ℓf-scaled
selected lifted product, primitivePart (centeredLiftPoly ((ℓf · ∏ S) % p^k)) = factor. This is the original-coordinate analogue of
RecoveredAtLift.candidate_eq_of_monic_dvd, but with no dilate; the proof just
transports the witness congr through the ℓf-scaling (scale_congr_of_congr).
A centred lift is coefficientwise congruent to its argument modulo m: each
coefficient is the centred representative centeredModNat, which differs from the
original by a multiple of m.
Coprimality with p ^ k makes the integer leading coefficient nonzero
in the prime field at p.
Reduction modulo p of an integer rescaling: the integer scalar reduces to
its ZMod64 p image, modP p (scale c f) = scale (↑c) (modP p f).
The BHKS monicTarget reduces mod p to the monic modular image of core.
Both are the monic mod-p factor pattern of core; the monicTarget realises it
as an honest reduction (ℓf⁻¹·core ≡ monicModularImage (modP p core)), provided
the prime is good for core and ℓf is coprime to p^k.
Abstract-bound variant of
existsUnique_recoveringLiftedFactorSubset_of_henselSubsetCorrespondence:
takes B' : Nat, hvalid : ∀ i, (factor.coeff i).natAbs ≤ B', and
hprecision : 2 * B' < d.p ^ d.k in place of the input-shape
defaultFactorCoeffBound core precision constraint. The body mirrors
the original but invokes the _of_bound recovery theorem instead of
the input-shape one.
Group A2 packaged for downstream exhaustive-search proofs: under the Hensel subset-correspondence hypotheses, each irreducible integer factor has a unique lifted-factor subset whose recovered-coordinate candidate equals the factor exactly at Mignotte precision.
This is a thin wrapper over
existsUnique_recoveringLiftedFactorSubset_of_henselSubsetCorrespondence_of_bound
that instantiates B' := defaultFactorCoeffBound core. The coefficient bound
is explicitly about the hidden monic-coordinate witness exposed by the
RecoveredAtLift carrier.
Induced subset-correspondence predicate for the recursive state of the exhaustive recombination search.
After the search consumes a prefix of subsets, it recurses on a target
polynomial (a quotient of core by the factors emitted so far) with a reduced
index set J ⊆ Finset.univ of lifted-factor indices not yet selected. This
predicate packages the correspondence between irreducible integer divisors of
target and their representing lifted-factor subsets, constrained to live in
J.
When target = core and J = Finset.univ, this reduces to the existence and
uniqueness fields of HenselSubsetCorrespondenceHypotheses. Downstream
coverage proofs use the predicate to track the recursive state across one
emission step at a time.
- exists_subset {factor : Hex.ZPoly} : Hex.normalizeFactorSign factor = factor → Irreducible (HexPolyZMathlib.toPolynomial factor) → factor ∣ target → ∃ S ⊆ J, RepresentsIntegerFactorAtLift core d factor S
Every normalized irreducible divisor has a representing subset inside
J. - unique_subset {factor : Hex.ZPoly} {S T : LiftedFactorSubset d} : Irreducible (HexPolyZMathlib.toPolynomial factor) → factor ∣ target → S ⊆ J → T ⊆ J → RepresentsIntegerFactorAtLift core d factor S → RepresentsIntegerFactorAtLift core d factor T → S = T
An irreducible divisor has at most one representing subset inside
J.
Instances For
Initial-state lemma: a Hensel subset correspondence implies the induced
predicate at the full universe of lifted-factor indices with target = core.
This is the entry point for downstream recursive-search coverage proofs.
A polynomial factor with nonnegative leading coefficient is a fixed point of
Hex.normalizeFactorSign.
Transport an induced Hensel subset correspondence through one emitted recombination factor.
The emitted subset S is removed from the remaining index set. The only
non-structural obligation is the expected disjointness fact: every irreducible
divisor of the quotient must be represented by a subset disjoint from the
emitted subset. Later coverage proofs discharge that from square-free
factorisation/associatedness; this lemma packages the pure rest-state transport
and reuses the parent state's uniqueness field.
Strengthened rest predicate that augments HenselSubsetCorrespondenceRest
with the structural facts needed by the recursive-coverage proof:
square-freeness of target in Polynomial ℤ, a cover field saying every
remaining index lies in some representing subset, a pairwise-disjoint
field for non-associated irreducible divisors, and a uniqueness-up-to-
association field saying associated irreducible divisors of target share
their representing subset.
The doc-comment on henselSubsetCorrespondenceRest_transport_of_disjoint
flags the disjointness obligation as "discharged from square-free
factorisation by later coverage proofs"; this predicate packages exactly
that information.
The predicate is designed to transport through one emitted recombination factor.
- exists_subset {factor : Hex.ZPoly} : Hex.normalizeFactorSign factor = factor → Irreducible (HexPolyZMathlib.toPolynomial factor) → factor ∣ target → ∃ S ⊆ J, RepresentsIntegerFactorAtLift core d factor S
- unique_subset {factor : Hex.ZPoly} {S T : LiftedFactorSubset d} : Irreducible (HexPolyZMathlib.toPolynomial factor) → factor ∣ target → S ⊆ J → T ⊆ J → RepresentsIntegerFactorAtLift core d factor S → RepresentsIntegerFactorAtLift core d factor T → S = T
- target_squarefree : Squarefree (HexPolyZMathlib.toPolynomial target)
The current target has no repeated irreducible factors.
- cover {i : LiftedFactorIndex d} : i ∈ J → ∃ (f : Hex.ZPoly) (S : LiftedFactorSubset d), Irreducible (HexPolyZMathlib.toPolynomial f) ∧ f ∣ target ∧ S ⊆ J ∧ i ∈ S ∧ RepresentsIntegerFactorAtLift core d f S
Every remaining lifted factor belongs to an irreducible divisor of the target.
- pairwise_disjoint {f g : Hex.ZPoly} {S T : LiftedFactorSubset d} : Irreducible (HexPolyZMathlib.toPolynomial f) → f ∣ target → S ⊆ J → RepresentsIntegerFactorAtLift core d f S → Irreducible (HexPolyZMathlib.toPolynomial g) → g ∣ target → T ⊆ J → RepresentsIntegerFactorAtLift core d g T → ¬Associated (HexPolyZMathlib.toPolynomial f) (HexPolyZMathlib.toPolynomial g) → Disjoint S T
Nonassociated irreducible factors have disjoint lifted supports.
- unique_up_to_associated {f g : Hex.ZPoly} {S T : LiftedFactorSubset d} : Irreducible (HexPolyZMathlib.toPolynomial f) → f ∣ target → S ⊆ J → RepresentsIntegerFactorAtLift core d f S → Irreducible (HexPolyZMathlib.toPolynomial g) → g ∣ target → T ⊆ J → RepresentsIntegerFactorAtLift core d g T → Associated (HexPolyZMathlib.toPolynomial f) (HexPolyZMathlib.toPolynomial g) → S = T
Associated irreducible factors have the same lifted support.
- support_subset_of_dvd_recombinationCandidate {f : Hex.ZPoly} {S T : LiftedFactorSubset d} : Irreducible (HexPolyZMathlib.toPolynomial f) → f ∣ target → T ⊆ J → Hex.DensePoly.leadingCoeff core = 1 → f ∣ liftedFactorProductCandidate d T → S ⊆ J → RepresentsIntegerFactorAtLift core d f S → S ⊆ T
Divisibility of a direct recombination candidate implies support inclusion.
- support_subset_of_dvd_liftedRecoveryCandidate {f : Hex.ZPoly} {S T : LiftedFactorSubset d} : Irreducible (HexPolyZMathlib.toPolynomial f) → f ∣ target → T ⊆ J → f ∣ liftedRecoveryCandidate core d T → S ⊆ J → RepresentsIntegerFactorAtLift core d f S → S ⊆ T
Divisibility of a recovered candidate implies support inclusion.
- liftedRecoveryCandidate_eq {f : Hex.ZPoly} {S : LiftedFactorSubset d} : Irreducible (HexPolyZMathlib.toPolynomial f) → f ∣ target → S ⊆ J → RepresentsIntegerFactorAtLift core d f S → liftedRecoveryCandidate core d S = f
Recovery from a genuine support returns its represented factor.
Instances For
The lifted-index supports corresponding to irreducible integer divisors of
core, represented at the Hensel lift by RepresentsIntegerFactorAtLift.
This is the concrete trueSupports family used by the BHKS support-partition
counting step: the executable representation is a Finset, while the lattice
side consumes supports as sets of lifted-factor indices.
The accompanying partition lemmas specialize to the full lifted-index universe
J = Finset.univ; proper recursive rest partitions keep their remaining-index
guard outside this support family.
Equations
- One or more equations did not get rendered due to their size.