Documentation

theorem HexBerlekampZassenhausMathlib.liftedIndex_mem_liftedSubset_iff (primeData : Hex.PrimeChoiceData) (d : Hex.LiftData) (hsize : d.liftedFactors.size = primeData.factorsModP.size) (S : ModPFactorSubset primeData) (i : ModPFactorIndex primeData) :

liftedIndexOfModPIndex primeData d hsize i ∈ liftedSubsetOfModPSubset primeData d hsize S ↔ i ∈ S

Membership in a lifted canonical subset, tested at the lifted image of a mod-p factor index, is exactly membership in the original mod-p subset.

theorem HexBerlekampZassenhausMathlib.liftedSubsetOfModPSubset_injective (primeData : Hex.PrimeChoiceData) (d : Hex.LiftData) (hsize : d.liftedFactors.size = primeData.factorsModP.size) :

Function.Injective (liftedSubsetOfModPSubset primeData d hsize)

The canonical lift from mod-p factor subsets to lifted-factor subsets is injective.

theorem HexBerlekampZassenhausMathlib.liftedSubsetOfModPSubset_disjoint_iff (primeData : Hex.PrimeChoiceData) (d : Hex.LiftData) (hsize : d.liftedFactors.size = primeData.factorsModP.size) (S T : ModPFactorSubset primeData) :

Disjoint (liftedSubsetOfModPSubset primeData d hsize S) (liftedSubsetOfModPSubset primeData d hsize T) ↔ Disjoint S T

Canonical lifting reflects and preserves disjointness.

noncomputable def HexBerlekampZassenhausMathlib.scaledLiftedFactorProduct (core : Hex.ZPoly) (d : Hex.LiftData) (S : LiftedFactorSubset d) :

Selected lifted-factor product scaled by the leading coefficient of the integer square-free part, matching the product formed by the executable recombination candidate checker.

Equations

HexBerlekampZassenhausMathlib.scaledLiftedFactorProduct core d S = Hex.DensePoly.scale (Hex.DensePoly.leadingCoeff core) (HexBerlekampZassenhausMathlib.liftedFactorProduct d S)

Instances For

structure HexBerlekampZassenhausMathlib.RecoveredAtLift (core : Hex.ZPoly) (d : Hex.LiftData) (factor : Hex.ZPoly) (S : LiftedFactorSubset d) :

Type

Corrected recovered-coordinate representation of an integer factor at a Hensel lift. The selected lifted product represents a monic-coordinate factor modulo p^k; dilating that monic factor by leadingCoeff core and taking primitive part recovers the integer factor of core.

The monic_dvd field pins the monic coordinate down to the canonical bounded representative: it must divide (toMonic core).monic, the monic polynomial the Hensel lift is actually built on. This forces a Mignotte coefficient bound on monicFactor (via defaultFactorCoeffBound_valid), which is what makes the exact-recovery lemma candidate_eq_of_bound applicable; without it the residue link alone admits non-canonical witnesses.

This is the data-bearing carrier behind the public proof-level RepresentsIntegerFactorAtLift predicate.

monicFactor : Hex.ZPoly
The monic-coordinate factor represented by the selected lifted factors.
congr : (liftedFactorProduct d S).reduceModPow d.p d.k = self.monicFactor.reduceModPow d.p d.k
The selected lifted product agrees with the monic factor modulo the lift modulus.
dilate_eq : (Hex.ZPoly.dilate (Hex.DensePoly.leadingCoeff core) self.monicFactor).primitivePart = factor
Dilation by the input leading coefficient recovers the original factor.
monic_dvd : self.monicFactor ∣ core.toMonic.monic
The monic-coordinate factor divides the transformed input.

Instances For

def HexBerlekampZassenhausMathlib.RepresentsIntegerFactorAtLift (core : Hex.ZPoly) (d : Hex.LiftData) (factor : Hex.ZPoly) (S : LiftedFactorSubset d) :

An integer factor is represented by a subset of the lifted local factors when the unscaled selected product recovers a monic-coordinate witness whose leading-coefficient dilation has primitive part equal to the integer factor.

The public predicate is proof-only; helper lemmas can unpack the underlying RecoveredAtLift witness when they need the monic-coordinate data.

Equations

HexBerlekampZassenhausMathlib.RepresentsIntegerFactorAtLift core d factor S = Nonempty (HexBerlekampZassenhausMathlib.RecoveredAtLift core d factor S)

Instances For

theorem HexBerlekampZassenhausMathlib.RepresentsIntegerFactorAtLift.ofRecovered {core factor : Hex.ZPoly} {d : Hex.LiftData} {S : LiftedFactorSubset d} (h : RecoveredAtLift core d factor S) :

RepresentsIntegerFactorAtLift core d factor S

Pack a data-bearing recovered-coordinate witness into the public predicate.

theorem HexBerlekampZassenhausMathlib.RepresentsIntegerFactorAtLift.elim {core factor : Hex.ZPoly} {d : Hex.LiftData} {S : LiftedFactorSubset d} {motive : Prop} (hrep : RepresentsIntegerFactorAtLift core d factor S) (h : ∀ (monicFactor : Hex.ZPoly), (liftedFactorProduct d S).reduceModPow d.p d.k = monicFactor.reduceModPow d.p d.k → (Hex.ZPoly.dilate (Hex.DensePoly.leadingCoeff core) monicFactor).primitivePart = factor → motive) :

motive

Eliminator exposing the monic-coordinate witness, its modular congruence, and the dilation equality locally.

noncomputable def HexBerlekampZassenhausMathlib.liftedFactorProductCandidate (d : Hex.LiftData) (S : LiftedFactorSubset d) :

Proof-side form of the executable recombination candidate, using the selected lifted-factor product directly. The executable-list version is introduced later, after the list-selection identification has been developed, and is proved equal to this definition.

Equations

HexBerlekampZassenhausMathlib.liftedFactorProductCandidate d S = Hex.normalizeFactorSign (Hex.centeredLiftPoly (HexBerlekampZassenhausMathlib.liftedFactorProduct d S) (d.p ^ d.k)).primitivePart

Instances For

noncomputable def HexBerlekampZassenhausMathlib.liftedRecoveryCandidate (core : Hex.ZPoly) (d : Hex.LiftData) (S : LiftedFactorSubset d) :

Proof-side candidate for recovering an integer factor of a possibly non-monic square-free part from a selected lifted-factor product. The selected product is first centred in the Hensel modulus, then transported back from the toMonic coordinate system by X ↦ leadingCoeff core * X, and finally made primitive with canonical sign.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem HexBerlekampZassenhausMathlib.liftedRecoveryCandidate.eq_productCandidate_of_lc_one {core : Hex.ZPoly} {d : Hex.LiftData} {S : LiftedFactorSubset d} (hlead : Hex.DensePoly.leadingCoeff core = 1) :

liftedRecoveryCandidate core d S = liftedFactorProductCandidate d S

On monic square-free parts, the recovered non-monic candidate collapses to the existing unscaled lifted-product candidate.

noncomputable def HexBerlekampZassenhausMathlib.scaledRecombinationCandidate (core : Hex.ZPoly) (d : Hex.LiftData) (S : LiftedFactorSubset d) :

Scaled variant of the recombination candidate: centred lift of the leading-coefficient-scaled selected lifted-factor product, primitivised and sign-normalised. This is the primitive non-monic supporting lemma used by the scaled recombination search.

Equations

One or more equations did not get rendered due to their size.

Instances For

structure HexBerlekampZassenhausMathlib.HenselSubsetCorrespondenceHypotheses (core : Hex.ZPoly) (B : ℕ) (primeData : Hex.PrimeChoiceData) (d : Hex.LiftData) (admissiblePrime successfulLift : Prop) :

Proof-facing package for the square-free Hensel subset correspondence over the executable PrimeChoiceData/LiftData surface.

The two proposition parameters are hooks for the precise admissible-prime and successful-lift hypotheses supplied by the later analytic Hensel proof. The caller theorems below depend only on the resulting existence and uniqueness fields, so downstream exhaustive-recombination proofs can be written against a stable executable API.

lift_eq : d = core.toMonicLiftData B primeData
The lift data is the lift selected from these inputs.
admissible_prime : admissiblePrime
The selected prime satisfies the caller's admissibility condition.
successful_lift : successfulLift
The multifactor Hensel lift satisfies the caller's success condition.
exists_subset {factor : Hex.ZPoly} : Hex.normalizeFactorSign factor = factor → Irreducible (HexPolyZMathlib.toPolynomial factor) → factor ∣ core → ∃ (S : LiftedFactorSubset d), RepresentsIntegerFactorAtLift core d factor S
Every normalized irreducible divisor has a representing lifted subset.
unique_subset {factor : Hex.ZPoly} {S T : LiftedFactorSubset d} : Irreducible (HexPolyZMathlib.toPolynomial factor) → factor ∣ core → RepresentsIntegerFactorAtLift core d factor S → RepresentsIntegerFactorAtLift core d factor T → S = T
The lifted subset representing an irreducible divisor is unique.

Instances For

structure HexBerlekampZassenhausMathlib.HenselSubsetLiftHypotheses (core : Hex.ZPoly) (B : ℕ) (primeData : Hex.PrimeChoiceData) (d : Hex.LiftData) (admissiblePrime squareFreeReduction successfulLift coprimeLift : Prop) :

Proof-facing package for transporting the mod-p subset partition through a successful Hensel lift.

The fields isolate the analytic Hensel obligations: the lift preserves the factor count, every mod-p selected subset represents the same integer factor after lifting, and every lifted representation descends to a mod-p selected subset. The caller theorems below combine these fields with ModPSubsetPartitionHypotheses to recover the existing lifted-subset correspondence API.

lift_eq : d = core.toMonicLiftData B primeData
The lift data is the lift selected from these inputs.
factor_count_eq : d.liftedFactors.size = primeData.factorsModP.size
The lift preserves the number of modular factors.
admissible_prime : admissiblePrime
The selected prime satisfies the caller's admissibility condition.
square_free_reduction : squareFreeReduction
Reduction modulo the selected prime preserves square-freeness.
successful_lift : successfulLift
The multifactor Hensel lift satisfies the caller's success condition.
coprime_lift : coprimeLift
The lifted factors satisfy the caller's coprimality condition.
represents_lifted_of_modP {factor : Hex.ZPoly} {S : ModPFactorSubset primeData} : Irreducible (HexPolyZMathlib.toPolynomial factor) → factor ∣ core → RepresentsIntegerFactorModP primeData factor S → RepresentsIntegerFactorAtLift core d factor (liftedSubsetOfModPSubset primeData d ⋯ S)
A modular representation gives a representation by the corresponding lifted factors.
represents_modP_of_lifted {factor : Hex.ZPoly} {T : LiftedFactorSubset d} : Irreducible (HexPolyZMathlib.toPolynomial factor) → factor ∣ core → RepresentsIntegerFactorAtLift core d factor T → ∃ (S : ModPFactorSubset primeData), T = liftedSubsetOfModPSubset primeData d ⋯ S ∧ RepresentsIntegerFactorModP primeData factor S
Every lifted representation descends to a corresponding modular representation.

Instances For

structure HexBerlekampZassenhausMathlib.HenselLiftDescentHypotheses (core : Hex.ZPoly) (B : ℕ) (primeData : Hex.PrimeChoiceData) (d : Hex.LiftData) (successfulLift coprimeLift : Prop) :

Explicit descent-only package for the lifted Hensel side.

This gives the reverse transport obligation a name independent of the full HenselSubsetCorrespondenceHypotheses API. Callers still have to prove the descent field; the point of the package is that they can combine that proof with forward Hensel transport without first constructing the lifted subset correspondence.

lift_eq : d = core.toMonicLiftData B primeData
The lift data is the lift selected from these inputs.
factor_count_eq : d.liftedFactors.size = primeData.factorsModP.size
The lift preserves the number of modular factors.
successful_lift : successfulLift
The multifactor Hensel lift satisfies the caller's success condition.
coprime_lift : coprimeLift
The lifted factors satisfy the caller's coprimality condition.
represents_modP_of_lifted {factor : Hex.ZPoly} {T : LiftedFactorSubset d} : Irreducible (HexPolyZMathlib.toPolynomial factor) → factor ∣ core → RepresentsIntegerFactorAtLift core d factor T → ∃ (S : ModPFactorSubset primeData), T = liftedSubsetOfModPSubset primeData d ⋯ S ∧ RepresentsIntegerFactorModP primeData factor S
Every lifted representation descends to a corresponding modular representation.

Instances For

structure HexBerlekampZassenhausMathlib.MonicDescent (core : Hex.ZPoly) (primeData : Hex.PrimeChoiceData) (d : Hex.LiftData) (factor : Hex.ZPoly) (T : LiftedFactorSubset d) (hsize : d.liftedFactors.size = primeData.factorsModP.size) :

Type

Data-bearing reverse descent from a monic-coordinate lift.

The lifted representation still recovers the original integer factor, but the descended mod-p subset represents the monic correspondent stored inside the RecoveredAtLift witness. This is the sound replacement for asking the same subset to represent the non-monic original factor modulo prime data selected for (toMonic core).monic.

modPSubset : ModPFactorSubset primeData
The modular subset underlying the selected lifted factors.
subset_eq : T = liftedSubsetOfModPSubset primeData d hsize self.modPSubset
Lifting the modular subset gives the original lifted subset.
recovered : RecoveredAtLift core d factor T
The lifted subset recovers the original-coordinate factor.
represents_monic : RepresentsIntegerFactorModP primeData self.recovered.monicFactor self.modPSubset
The modular subset represents the recovered monic-coordinate factor.

Instances For

def HexBerlekampZassenhausMathlib.MonicDescent.ofRecovered {core factor : Hex.ZPoly} {primeData : Hex.PrimeChoiceData} {d : Hex.LiftData} {T : LiftedFactorSubset d} {hsize : d.liftedFactors.size = primeData.factorsModP.size} (S : ModPFactorSubset primeData) (hT : T = liftedSubsetOfModPSubset primeData d hsize S) (hrec : RecoveredAtLift core d factor T) (hmod : RepresentsIntegerFactorModP primeData hrec.monicFactor S) :

MonicDescent core primeData d factor T hsize

Pack the explicit monic-correspondent reverse-descent fields.

Equations

HexBerlekampZassenhausMathlib.MonicDescent.ofRecovered S hT hrec hmod = { modPSubset := S, subset_eq := hT, recovered := hrec, represents_monic := hmod }

Instances For

theorem HexBerlekampZassenhausMathlib.MonicDescent.dilate_eq {core factor : Hex.ZPoly} {primeData : Hex.PrimeChoiceData} {d : Hex.LiftData} {T : LiftedFactorSubset d} {hsize : d.liftedFactors.size = primeData.factorsModP.size} (h : MonicDescent core primeData d factor T hsize) :

(Hex.ZPoly.dilate (Hex.DensePoly.leadingCoeff core) h.recovered.monicFactor).primitivePart = factor

Projection of the original-factor recovery equality.

theorem HexBerlekampZassenhausMathlib.MonicDescent.monic_dvd {core factor : Hex.ZPoly} {primeData : Hex.PrimeChoiceData} {d : Hex.LiftData} {T : LiftedFactorSubset d} {hsize : d.liftedFactors.size = primeData.factorsModP.size} (h : MonicDescent core primeData d factor T hsize) :

h.recovered.monicFactor ∣ core.toMonic.monic

Projection that the monic correspondent divides the monic transform.

structure HexBerlekampZassenhausMathlib.MonicDescentHypotheses (core : Hex.ZPoly) (B : ℕ) (primeData : Hex.PrimeChoiceData) (d : Hex.LiftData) (successfulLift coprimeLift : Prop) :

Descent-only package for the to-monic reverse direction.

Unlike HenselLiftDescentHypotheses, this package does not claim that a lifted representation of the original non-monic factor descends to a mod-p representation of that same factor. It descends to the monic correspondent recorded by RecoveredAtLift, while retaining the dilation equality back to the original factor.

lift_eq : d = core.toMonicLiftData B primeData
The lift data is the lift selected from these inputs.
factor_count_eq : d.liftedFactors.size = primeData.factorsModP.size
The lift preserves the number of modular factors.
successful_lift : successfulLift
The multifactor Hensel lift satisfies the caller's success condition.
coprime_lift : coprimeLift
The lifted factors satisfy the caller's coprimality condition.
descends {factor : Hex.ZPoly} {T : LiftedFactorSubset d} : Irreducible (HexPolyZMathlib.toPolynomial factor) → factor ∣ core → RepresentsIntegerFactorAtLift core d factor T → ∃ (S : ModPFactorSubset primeData) (hrec : RecoveredAtLift core d factor T), T = liftedSubsetOfModPSubset primeData d ⋯ S ∧ RepresentsIntegerFactorModP primeData hrec.monicFactor S
A lifted representation descends to its modular subset and monic correspondent.

Instances For

theorem HexBerlekampZassenhausMathlib.liftedRecoveryCandidate_eq_factor_of_congruence_of_bound {core factor monicFactor : Hex.ZPoly} {d : Hex.LiftData} {S : LiftedFactorSubset d} (B' : ℕ) (hvalid : ∀ (i : ℕ), (Hex.DensePoly.coeff monicFactor i).natAbs ≤ B') (hcong : (liftedFactorProduct d S).reduceModPow d.p d.k = monicFactor.reduceModPow d.p d.k) (hdilate : (Hex.ZPoly.dilate (Hex.DensePoly.leadingCoeff core) monicFactor).primitivePart = factor) (hfactor_norm : Hex.normalizeFactorSign factor = factor) (hprecision : 2 * B' < d.p ^ d.k) :

liftedRecoveryCandidate core d S = factor

Precision-conditional exact recovery for liftedRecoveryCandidate in the dilation-coordinate model.

theorem HexBerlekampZassenhausMathlib.RecoveredAtLift.candidate_eq_of_bound {core factor : Hex.ZPoly} {d : Hex.LiftData} {S : LiftedFactorSubset d} (hrep : RecoveredAtLift core d factor S) (B' : ℕ) (hvalid : ∀ (i : ℕ), (Hex.DensePoly.coeff hrep.monicFactor i).natAbs ≤ B') (hfactor_norm : Hex.normalizeFactorSign factor = factor) (hprecision : 2 * B' < d.p ^ d.k) :

liftedRecoveryCandidate core d S = factor

Exact recovery of the executable recovered candidate from the corrected monic-coordinate representation carrier.

theorem HexBerlekampZassenhausMathlib.RecoveredAtLift.candidate_eq_of_monic_dvd {core factor : Hex.ZPoly} {d : Hex.LiftData} {S : LiftedFactorSubset d} (hrep : RecoveredAtLift core d factor S) (hmonic_ne : core.toMonic.monic ≠ 0) (hfactor_norm : Hex.normalizeFactorSign factor = factor) (hprecision : 2 * core.toMonic.monic.defaultFactorCoeffBound < d.p ^ d.k) :

liftedRecoveryCandidate core d S = factor

Exact recovery driven directly by the carrier's monic_dvd field.

This is the producer half of the recovery contract: the monic_dvd field forces monicFactor ∣ (toMonic core).monic, so defaultFactorCoeffBound_valid discharges the Mignotte coefficient bound at B' := defaultFactorCoeffBound (toMonic core).monic with no separate validity obligation on the caller. The only remaining precision hypothesis is that the Hensel modulus clears twice that bound.

theorem HexBerlekampZassenhausMathlib.centeredLift_scaledLiftedFactorProduct_eq_of_mignottePrecision_of_bound {core factor : Hex.ZPoly} {d : Hex.LiftData} {S : LiftedFactorSubset d} (B' : ℕ) (hvalid : ∀ (i : ℕ), (Hex.DensePoly.coeff factor i).natAbs ≤ B') (hscaled : (scaledLiftedFactorProduct core d S).reduceModPow d.p d.k = factor.reduceModPow d.p d.k) (hprecision : 2 * B' < d.p ^ d.k) :

Hex.centeredLiftPoly ((scaledLiftedFactorProduct core d S).reduceModPow d.p d.k) (d.p ^ d.k) = factor

Abstract-bound variant of centeredLift_scaledLiftedFactorProduct_eq_of_mignottePrecision: takes an arbitrary B' : Nat, an explicit validity hypothesis hvalid : ∀ i, (factor.coeff i).natAbs ≤ B', and the scaled-product congruence in place of the public representation predicate. The body just threads B' and hvalid into centeredLiftPoly_eq_of_reduceModPow_eq (which already accepts an abstract bound). The original input-shape theorem is a wrapper around this variant.