structure HexBerlekampZassenhausMathlib.ModPFactorization (f : Hex.ZPoly) (data : Hex.PrimeChoiceData) : Prop

Semantic validity of data as a mod-p factorization package for the monic lift target f: everything the certification cone consumes about a PrimeChoiceData, with no reference to how it was produced.

• prime : Hex.Nat.Prime data.p

  The selected modulus is prime.

• good : Hex.isGoodPrime f data.p = true

  The prime satisfies the executable admissibility test for f.

• fModP_eq : data.fModP = Hex.ZPoly.modP data.p f

  The cached modular polynomial is the reduction of f.

• monic (g : Hex.FpPoly data.p) : g ∈ data.factorsModP → Hex.DensePoly.Monic g

  Every modular factor is monic.

• ne_nil : data.factorsModP.toList ≠ []

  The modular factor list is nonempty.

• nodup : data.factorsModP.toList.Nodup

  No modular factor occurs twice.

• coprime : Hex.ZPoly.QuadraticMultifactorCoprimeSplits data.p data.factorsModP.toList

  The splits used for the multifactor lift are pairwise coprime.

• irreducible (i : ModPFactorIndex data) : Irreducible (HexPolyFpMathlib.toMathlibPolynomial (modPFactor data i))

  Every indexed modular factor is irreducible.

• product : (Array.map Hex.FpPoly.liftToZ data.factorsModP).polyProduct.congr (Hex.monicModularImage (Hex.ZPoly.modP data.p f)).liftToZ data.p

  The product of the lifted factors agrees with the monic modular image.

• natDegree_pos (g : Hex.FpPoly data.p) : g ∈ data.factorsModP → 0 < (HexPolyZMathlib.toPolynomial g.liftToZ).natDegree

  Every modular factor has positive degree.

theorem HexBerlekampZassenhausMathlib.modP_polyProduct_map_liftToZ {p : ℕ} [Hex.ZMod64.Bounds p] (arr : Array (Hex.FpPoly p)) : Hex.ZPoly.modP p (Array.map Hex.FpPoly.liftToZ arr).polyProduct = List.foldl (fun (x1 x2 : Hex.FpPoly p) => x1 * x2) 1 arr.toList

The modP/liftToZ roundtrip on an FpPoly product: reducing the integer product of the lifts recovers the FpPoly fold product.

theorem HexBerlekampZassenhausMathlib.modPFactorization_of_form {f : Hex.ZPoly} {data : Hex.PrimeChoiceData} (hprime : Hex.Nat.Prime data.p) (hgood : Hex.isGoodPrime f data.p = true) (hfmod : data.fModP = Hex.ZPoly.modP data.p f) (hform : Hex.factorsModPBerlekampForm f data) (hprim : f.Primitive) (hlc_pos : 0 < Hex.DensePoly.leadingCoeff f) (hpos : 0 < Hex.DensePoly.natDegree f) : ModPFactorization f data

Assemble the semantic bundle from a proved Berlekamp-form factorization. The lift target must be primitive with positive leading coefficient and positive degree.

theorem HexBerlekampZassenhausMathlib.modPFactorization_of_choosePrimeData {f : Hex.ZPoly} {data : Hex.PrimeChoiceData} (hchoose : Hex.choosePrimeData? f = some data) (hprim : f.Primitive) (hlc_pos : 0 < Hex.DensePoly.leadingCoeff f) (hpos : 0 < Hex.DensePoly.natDegree f) : ModPFactorization f data

The selection witness yields the semantic bundle through the choosePrimeData? extraction lemmas.

theorem HexBerlekampZassenhausMathlib.modPFactorization_of_probePrimeData {f : Hex.ZPoly} {candidate : Hex.SmallPrimeCandidate} {data : Hex.PrimeChoiceData} (hprobe : Hex.probePrimeData? f candidate = some data) (hprim : f.Primitive) (hlc_pos : 0 < Hex.DensePoly.leadingCoeff f) (hpos : 0 < Hex.DensePoly.natDegree f) : ModPFactorization f data

An explicit cached prime trial yields the semantic modular factorization bundle consumed by direct lifting.

theorem HexBerlekampZassenhausMathlib.ModPFactorization.factorCount_le_degree_of_product {f target : Hex.ZPoly} {data : Hex.PrimeChoiceData} (h : ModPFactorization f data) (hmonic : Hex.DensePoly.Monic target) (hcongr : (Array.map Hex.FpPoly.liftToZ data.factorsModP).polyProduct.congr target data.p) : data.factorsModP.size ≤ Hex.DensePoly.natDegree target

A modular factor array of positive-degree monic factors has no more entries than the degree of any monic integer target to which its product is congruent.