theorem HexBerlekampZassenhausMathlib.exists_factor_of_modPIndex (core : Hex.ZPoly) (hcore_ne : core ≠ 0) (_hcore_pos : 0 < Hex.DensePoly.natDegree core) (primeData : Hex.PrimeChoiceData) (hval : ModPFactorization core primeData) (i : ModPFactorIndex primeData) : ∃ (g : Hex.ZPoly), Irreducible (HexPolyZMathlib.toPolynomial g) ∧ g ∣ core ∧ HexPolyFpMathlib.toMathlibPolynomial (modPFactor primeData i) ∣ HexPolyFpMathlib.toMathlibPolynomial (monicModPImage (Hex.ZPoly.modP primeData.p g))

For every indexed modular factor selected by a successful choosePrimeData? run, recover an irreducible integer divisor whose monic mod-p image is divisible by that indexed factor.

theorem HexBerlekampZassenhausMathlib.existsUnique_modPFactorSubset_of_choosePrimeData_of_some (core : Hex.ZPoly) {factor : Hex.ZPoly} (_hirr : Irreducible (HexPolyZMathlib.toPolynomial factor)) (hdvd : factor ∣ core) (hcore_ne : core ≠ 0) (_hcore_pos : 0 < Hex.DensePoly.natDegree core) (primeData : Hex.PrimeChoiceData) (hval : ModPFactorization core primeData) : ∃! S : ModPFactorSubset primeData, RepresentsIntegerFactorModP primeData factor S

Final assembly: the analyzable choosePrimeData? core = some primeData branch of the integer-irreducible → mod-p representing-subset existence and uniqueness statement.

theorem HexBerlekampZassenhausMathlib.existsUnique_modPFactorSubset_of_modPFactorization (core : Hex.ZPoly) {factor : Hex.ZPoly} (primeData : Hex.PrimeChoiceData) (hirr : Irreducible (HexPolyZMathlib.toPolynomial factor)) (hdvd : factor ∣ core) (hcore_pos : 0 < Hex.DensePoly.natDegree core) (hval : ModPFactorization core primeData) : ∃! S : ModPFactorSubset primeData, RepresentsIntegerFactorModP primeData factor S

Caller-facing wrapper for the witness-form Hex.choosePrimeData? core = some primeData branch required by the ModPSubsetPartitionHypotheses constructor. The explicit hchoose witness excludes the none branch where the mod-p factorisation invariant is unavailable.

theorem HexBerlekampZassenhausMathlib.modPSubsetPartitionHypotheses_of_modPFactorization (core : Hex.ZPoly) (primeData : Hex.PrimeChoiceData) (hcore_pos : 0 < Hex.DensePoly.natDegree core) (hval : ModPFactorization core primeData) : ModPSubsetPartitionHypotheses core primeData True True

Construct ModPSubsetPartitionHypotheses at the executable Hex.choosePrimeData boundary.

Composes:

• Hex.choosePrimeData?_fModP_eq for fModP_eq;

• trivial for the True admissible_prime / square_free_reduction hooks;

• factors_irreducible_of_choosePrimeData_of_some for the per-factor irreducibility component;

• existsUnique_modPFactorSubset_of_choosePrimeData for both the existence and uniqueness components.

The hchoose hypothesis is an explicit choosePrimeData? = some witness, so the none branch (where the mod-p factorisation invariant is unavailable) is excluded; downstream callers discharge it from the same choosePrimeData? chain that supplies the other partition fields.

theorem HexBerlekampZassenhausMathlib.core_ne_zero_of_modPFactorization (core : Hex.ZPoly) (primeData : Hex.PrimeChoiceData) (hval : ModPFactorization core primeData) : core ≠ 0

A successful choosePrimeData? run forces a nonzero square-free part: the selected prime is isGoodPrime, which keeps (modP p core) nonzero, whereas modP p 0 = 0.

theorem HexBerlekampZassenhausMathlib.toMathlibPolynomial_modPFactor_injective_of_modPFactorization (core : Hex.ZPoly) (primeData : Hex.PrimeChoiceData) (hval : ModPFactorization core primeData) : Function.Injective fun (i : ModPFactorIndex primeData) => HexPolyFpMathlib.toMathlibPolynomial (modPFactor primeData i)

The Mathlib images of the selected modular factors are distinct: choosePrimeData? guarantees factorsModP.toList.Nodup, and toMathlibPolynomial is injective.

theorem HexBerlekampZassenhausMathlib.toMathlibPolynomial_modPFactor_monic_of_modPFactorization (core : Hex.ZPoly) (primeData : Hex.PrimeChoiceData) (hval : ModPFactorization core primeData) (i : ModPFactorIndex primeData) : (HexPolyFpMathlib.toMathlibPolynomial (modPFactor primeData i)).Monic

The Mathlib images of the selected modular factors are monic: choosePrimeData? guarantees each factorsModP entry is monic, preserved by toMathlibPolynomial.

theorem HexBerlekampZassenhausMathlib.modPFactor_index_cover (core : Hex.ZPoly) (primeData : Hex.PrimeChoiceData) (hcore_pos : 0 < Hex.DensePoly.natDegree core) (hval : ModPFactorization core primeData) (i : ModPFactorIndex primeData) : ∃ (g : Hex.ZPoly) (S : ModPFactorSubset primeData), Irreducible (HexPolyZMathlib.toPolynomial g) ∧ g ∣ core ∧ i ∈ S ∧ RepresentsIntegerFactorModP primeData g S

modP cover. Every selected modular factor index lies in the representing subset of some irreducible integer divisor of core.

Assembled from exists_factor_of_modPIndex (recover an irreducible divisor g whose monic mod-p image the indexed factor divides), the subset-partition existence projection (a representing subset S for g), and mem_modPSubset_of_dvd (the divisibility forces i ∈ S).