theorem HexBerlekampZassenhausMathlib.polyProduct_directSelectedFactors (d : Hex.LiftData) (selected : List (Hex.DirectLiftedIndex d)) (hnodup : selected.Nodup) : (Hex.directSelectedFactors d selected).toArray.polyProduct = liftedFactorProduct d selected.toFinset

An indexed support list with no duplicate indices has the proof-side finite-set product, independently of its traversal order.

theorem HexBerlekampZassenhausMathlib.directCandidate_indexed_eq (core : Hex.ZPoly) (d : Hex.LiftData) (selected : List (Hex.DirectLiftedIndex d)) (hnodup : selected.Nodup) : Hex.directCandidate (Hex.DensePoly.leadingCoeff core) (d.p ^ d.k) (Hex.directSelectedFactors d selected) = scaledRecombinationCandidate core d selected.toFinset

The indexed executable candidate agrees with the proof-side candidate on the finite support represented by the list.

theorem HexBerlekampZassenhausMathlib.gcd_primePow_eq_one_of_cast_ne_zero (a : ℤ) (p k : ℕ) (hp : Nat.Prime p) (ha : ↑a ≠ 0) : a.gcd (Int.ofNat (p ^ k)) = 1

A nonzero integer whose residue modulo a prime is nonzero is coprime to every positive power of that prime.

theorem HexBerlekampZassenhausMathlib.gcd_eq_one_of_dvd_left {a b m : ℤ} (hab : a ∣ b) (hb : b.gcd m = 1) : a.gcd m = 1

Coprimality with a modulus descends along divisibility of integer leading coefficients.

theorem HexBerlekampZassenhausMathlib.directScaledProduct_congr_of_modP_support {core factor cofactor : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} {S : ModPFactorSubset data} (hval : ModPFactorization core data) (hcore_size : 0 < Hex.DensePoly.size core) (hfactor_size : 0 < Hex.DensePoly.size factor) (hproduct : factor * cofactor = core) (hcore_lc : Hex.DensePoly.leadingCoeff core = Hex.DensePoly.leadingCoeff factor * Hex.DensePoly.leadingCoeff cofactor) (hgcd_core : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) (hgcd_factor : (Hex.DensePoly.leadingCoeff factor).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) (hgcd_cofactor : (Hex.DensePoly.leadingCoeff cofactor).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) (hprecision_pos : 1 ≤ Hex.precisionForCoeffBound B data.p) (hrep : RepresentsIntegerFactorModP data factor S) : let d := core.directLiftData B data; have T := liftedSubsetOfModPSubset data d ⋯ S; (scaledLiftedFactorProduct core d T).congr (Hex.DensePoly.scale (Hex.DensePoly.leadingCoeff cofactor) factor) (d.p ^ d.k)

The exact proportionality certificate behind direct recovery.

For an integer factor represented by a modular support, the leading-coefficient-scaled product of the corresponding canonical Hensel factors is congruent to the factor scaled by the leading coefficient of its cofactor. CLD consumes this statement directly; classical recovery additionally centers and primitivizes it.

theorem HexBerlekampZassenhausMathlib.directCandidate_eq_of_modP_support {core factor cofactor : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} {S : ModPFactorSubset data} (hval : ModPFactorization core data) (hcore_size : 0 < Hex.DensePoly.size core) (hfactor_size : 0 < Hex.DensePoly.size factor) (hproduct : factor * cofactor = core) (hcore_lc : Hex.DensePoly.leadingCoeff core = Hex.DensePoly.leadingCoeff factor * Hex.DensePoly.leadingCoeff cofactor) (hgcd_core : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) (hgcd_factor : (Hex.DensePoly.leadingCoeff factor).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) (hgcd_cofactor : (Hex.DensePoly.leadingCoeff cofactor).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) (hcofactor_lc_pos : 0 < Hex.DensePoly.leadingCoeff cofactor) (hfactor_prim : factor.primitivePart = factor) (hfactor_norm : Hex.normalizeFactorSign factor = factor) (hprecision_pos : 1 ≤ Hex.precisionForCoeffBound B data.p) (hprecision : 2 * core.defaultFactorCoeffBound < data.p ^ Hex.precisionForCoeffBound B data.p) (hrep : RepresentsIntegerFactorModP data factor S) : let d := core.directLiftData B data; scaledRecombinationCandidate core d (liftedSubsetOfModPSubset data d ⋯ S) = factor

Direct M1 recovery from one modular support.

The Hensel subset is lifted against monicTarget core; Hensel uniqueness identifies it with monicTarget factor. Scaling by lc(core) then recovers lc(cofactor) • factor, and primitive/sign normalization removes precisely that positive scalar.