The executable recombination candidate associated to a lifted-factor
subset: this is the Hex.ZPoly value that the recombination search compares
against the running target via shouldRecordPolynomialFactor /
exactQuotient?. Definitionally equal to the inline expression used inside
Hex.recombinationSearchModAux.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The executable-list recombination candidate agrees with the proof-side product candidate.
On monic square-free parts, the recovered non-monic candidate is the executable unscaled recombination candidate.
Membership correspondence between the two recombination enumerators: every
(selected, rest) partition the size-ordered enumerator
subsetsOfSizeWithComplement produces is also an (order-preserving) member of
the full subsetSplits enumeration. Both enumerators range over exactly the
order-preserving partitions of the list; only their visitation order differs.
This lets the size-ordered (smart) search reuse the subsetSplits subset
machinery.
Identify a split produced by the size-ordered (smart) recombination enumerator with a lifted-factor subset.
At the top level the smart search forces the head lifted factor into the
selected component and partitions the remaining tail by
subsetsOfSizeWithComplement. Every such split (head :: sc_sel, sc_rest) is
the (selected, rejected) list partition of a lifted-factor subset S: its
selected sublist is liftedSubsetSelectedList d S, hence its product is the
proof-side liftedFactorProduct d S, and the executable scaled candidate built
from the selected product (with coreLc = leadingCoeff core and
modulus = d.p ^ d.k) is exactly the proof-side
liftedRecoveryCandidate core d S.
Existence of the identifying subset needs no distinctness hypothesis; the
subset is recovered from the mask over the matched index list, which is
intrinsically Nodup. Distinctness of the lifted factors is what pins the
subset uniquely; that is supplied separately by
subsetsOfSizeWithComplement_liftedFactors_exists_unique_subset.
The selected-list map of a lifted-factor subset determines the subset when
the lifted factors are distinct: liftedSubsetSelectedList d is injective in
S whenever liftedFactor d is injective. This is the support-uniqueness step
used by direct recombination completeness.
Full identification of a size-ordered (smart) enumerator split with its
lifted-factor subset: when the lifted factors are distinct the subset S is
unique, so the executable candidate the search forms is identified with the
single proof-side liftedRecoveryCandidate core d S.
This packages subsetsOfSizeWithComplement_liftedFactors_exists_subset with the
distinctness-driven uniqueness, taking Function.Injective (liftedFactor d) as
an explicit hypothesis.
On a monic polynomial, the partition's lifted-recovery equality upgrades to the executable recombination-candidate equality consumed by the search recursion.
The partition's liftedRecoveryCandidate_eq field soundly pins the recovered
candidate liftedRecoveryCandidate core d S to the represented factor f; on a
monic polynomial, liftedRecoveryCandidate.eq_recombinationCandidate_of_lc_one
rewrites that into the unscaled executable recombinationCandidate d S. This is
the sound replacement for passing RepresentsIntegerFactorAtLift to the old
scaled-product modular recovery lemmas.
Abstract-bound variant of
centeredLiftPoly_scaledLiftedFactorProduct_eq_factor_of_recovery:
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 A2 recovery equality reformulated against the executable centred-lift
of the scaled lifted product, ready to feed downstream packaging that
relates the scaled centered lift to the unscaled recombinationCandidate.
This is the cleanest form in which the proof-side recovery is expressed for
later integration with executable-side normalisation reasoning (which removes
the lc(core) scale and chooses a sign).
This is a thin wrapper over
centeredLiftPoly_scaledLiftedFactorProduct_eq_factor_of_recovery_of_bound
that instantiates B' := defaultFactorCoeffBound core and discharges
hvalid via defaultFactorCoeffBound_valid core hcore_ne factor hdvd.
Direct-coordinate proportional recovery.
The selected monic Hensel product is scaled by leadingCoeff core; for a
proper factor this is congruent to c • factor, where c is the cofactor's
positive leading coefficient. Once that proportional polynomial lies in the
centred recovery window, primitivePart removes c and the executable direct
candidate is exactly factor.
Default-bound wrapper for direct proportional recovery from an explicit factor/cofactor product.
Abstract-bound variant of
recombinationCandidate_eq_factor_of_recovery_of_monic_core: 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 proof mirrors
the input-shape original but invokes
centeredLiftPoly_scaledLiftedFactorProduct_eq_factor_of_recovery_of_bound
in place of the input-shape recovery theorem.
Under a monic polynomial hypothesis, the scaled recovery theorem identifies the
unscaled executable recombination candidate with the represented integer
factor. This is the original-coordinate recovery statement; the older
recombinationCandidate_eq_factor_of_recovery wrapper also accepts the
executable record-filter hypothesis needed by some callers.
This is a thin wrapper over
recombinationCandidate_eq_factor_of_recovery_of_monic_core_of_bound
that instantiates B' := defaultFactorCoeffBound core and discharges
hvalid via defaultFactorCoeffBound_valid core hcore_ne factor hdvd.
Abstract-bound variant of
recombinationCandidate_eq_factor_of_recovery: 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. Delegates to
recombinationCandidate_eq_factor_of_recovery_of_monic_core_of_bound.
Under a monic polynomial hypothesis, the scaled recovery theorem identifies the unscaled executable recombination candidate with the represented integer factor.
This is a thin wrapper over
recombinationCandidate_eq_factor_of_recovery_of_bound that instantiates
B' := defaultFactorCoeffBound core and discharges hvalid via
defaultFactorCoeffBound_valid core hcore_ne factor hdvd.
Abstract-bound variant of
recombinationCandidate_eq_factor_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. Delegates to
recombinationCandidate_eq_factor_of_recovery_of_bound.
Hensel-correspondence wrapper for the monic polynomial recovery theorem.
Once a proof-side subset is known to represent an irreducible integer divisor at the Hensel lift, the executable recombination candidate is exactly that factor under the monic/primitive/sign-normalised hypotheses required by the centered-lift recovery bound.
This is a thin wrapper over
recombinationCandidate_eq_factor_of_henselSubsetCorrespondence_of_bound
that instantiates B' := defaultFactorCoeffBound core and discharges
hvalid via defaultFactorCoeffBound_valid core hcore_ne factor hdvd.
Abstract-bound variant of
scaledRecombinationCandidate_eq_factor_of_recovery: 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 centered-lift recovery theorem
instead of the input-shape one. The original input-shape theorem is a
wrapper around this variant.
The scaled recombination candidate
equals the represented integer factor under primitive/sign-normalised
hypotheses on factor plus the standard Mignotte-precision and representation
hypotheses.
Unlike recombinationCandidate_eq_factor_of_recovery_of_monic_core, this
theorem does not require Monic core and does not use the
leading-coefficient collapse scaledLiftedFactorProduct = liftedFactorProduct.
The inner equality is supplied directly by
centeredLiftPoly_scaledLiftedFactorProduct_eq_factor_of_recovery;
primitivePart_eq_self_of_primitive and the supplied normalizeFactorSign
fixed-point discharge the outer normalisation computation.
Callers use this in place of the monic polynomial recovery when the input hypotheses are
core ≠ 0 ∧ Primitive core ∧ 0 < leadingCoeff core; the primitive/sign
hypotheses on factor are supplied by their primitive-factor packaging step.
This is a thin wrapper over
scaledRecombinationCandidate_eq_factor_of_recovery_of_bound that
instantiates B' := defaultFactorCoeffBound core and discharges
hvalid via defaultFactorCoeffBound_valid core hcore_ne factor hdvd.
Abstract-bound variant of
scaledRecombinationCandidate_eq_factor_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. Body is a
one-line delegation to
scaledRecombinationCandidate_eq_factor_of_recovery_of_bound.
Hensel-correspondence wrapper for the primitive-polynomial scaled recovery theorem.
Primitive-polynomial analogue of
recombinationCandidate_eq_factor_of_henselSubsetCorrespondence: once a
proof-side subset is known to represent an irreducible integer divisor at the
Hensel lift, the scaled recombination candidate is exactly that factor under
the primitive/sign-normalised hypotheses required by the centered-lift
recovery bound.
This is a thin wrapper over
scaledRecombinationCandidate_eq_factor_of_henselSubsetCorrespondence_of_bound
that instantiates B' := defaultFactorCoeffBound core and discharges
hvalid via defaultFactorCoeffBound_valid core hcore_ne factor hdvd.