@[reducible, inline]

abbrev HexBerlekampZassenhausMathlib.ModPFactorIndex (primeData : Hex.PrimeChoiceData) : Type

Index type for the modular factors stored in executable prime-choice data.

Equations

• HexBerlekampZassenhausMathlib.ModPFactorIndex primeData = Fin primeData.factorsModP.size

@[reducible, inline]

abbrev HexBerlekampZassenhausMathlib.ModPFactorSubset (primeData : Hex.PrimeChoiceData) : Type

A finite subset of the modular factors stored in executable prime-choice data.

Equations

• HexBerlekampZassenhausMathlib.ModPFactorSubset primeData = Finset (HexBerlekampZassenhausMathlib.ModPFactorIndex primeData)

def HexBerlekampZassenhausMathlib.modPFactor (primeData : Hex.PrimeChoiceData) (i : ModPFactorIndex primeData) : Hex.FpPoly primeData.p

The selected modular factor at an executable PrimeChoiceData index.

Equations

• HexBerlekampZassenhausMathlib.modPFactor primeData i = primeData.factorsModP[i]

noncomputable def HexBerlekampZassenhausMathlib.modPFactorProduct (primeData : Hex.PrimeChoiceData) (S : ModPFactorSubset primeData) : Hex.FpPoly primeData.p

Product of the selected modular factors.

Equations

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

theorem HexBerlekampZassenhausMathlib.toMathlibPolynomial_modPFactorProduct (primeData : Hex.PrimeChoiceData) (S : ModPFactorSubset primeData) : HexPolyFpMathlib.toMathlibPolynomial (modPFactorProduct primeData S) = ∏ i ∈ S, HexPolyFpMathlib.toMathlibPolynomial (modPFactor primeData i)

Identify the executable modular subset product with a Mathlib Finset.prod.

The executable surface stores subset products as a left fold over Finset.toList; after transporting each FpPoly to Mathlib, commutativity identifies that fold with the canonical finite-set product.

def HexBerlekampZassenhausMathlib.monicModPImage {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) : Hex.FpPoly p

The monic modular image used for subset partition statements. This mirrors the executable prime-choice normalization: zero stays zero, and nonzero inputs are scaled by the inverse of their leading coefficient.

Equations

• HexBerlekampZassenhausMathlib.monicModPImage f = if Hex.DensePoly.isZero f = true then 0 else Hex.DensePoly.scale (Hex.DensePoly.leadingCoeff f)⁻¹ f

theorem HexBerlekampZassenhausMathlib.monicModPImage_eq_monicModularImage {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) : monicModPImage f = Hex.monicModularImage f

The proof-facing and executable monic modular images are the same polynomial.

theorem HexBerlekampZassenhausMathlib.monicModPImage_zero {p : ℕ} [Hex.ZMod64.Bounds p] : monicModPImage 0 = 0

The monic modular image of the zero polynomial is zero.

theorem HexBerlekampZassenhausMathlib.monicModPImage_ne_zero_of_ne_zero {p : ℕ} [Hex.ZMod64.Bounds p] [Fact (Hex.Nat.Prime p)] {f : Hex.FpPoly p} (hf : Hex.DensePoly.isZero f = false) : monicModPImage f ≠ 0

The monic modular image of a nonzero polynomial is nonzero.

theorem HexBerlekampZassenhausMathlib.monicModPImage_monic_of_ne_zero {p : ℕ} [Hex.ZMod64.Bounds p] (hprime : Hex.Nat.Prime p) {f : Hex.FpPoly p} (hf : Hex.DensePoly.isZero f = false) : Hex.DensePoly.Monic (monicModPImage f)

The monic modular image of a nonzero polynomial over a prime field is monic.

theorem HexBerlekampZassenhausMathlib.fpPoly_leadingCoeff_ne_zero_of_size_pos {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) (hf_size_pos : 0 < Hex.DensePoly.size f) : Hex.DensePoly.leadingCoeff f ≠ 0

Nonvanishing of the leading coefficient for a positive-size Hex.FpPoly p. Composes Hex.FpPoly.leadingCoeff_eq_coeff_pred, which rewrites the leading coefficient to f.coeff (f.size - 1), with Hex.DensePoly.coeff_last_ne_zero_of_pos_size, the invariant that the size-pred coefficient of a positive-size Hex.DensePoly is nonzero.

theorem HexBerlekampZassenhausMathlib.monicModPImage_dvd_self_of_ne_zero {p : ℕ} [Hex.ZMod64.Bounds p] (hprime : Hex.Nat.Prime p) {f : Hex.FpPoly p} (hf : Hex.DensePoly.isZero f = false) : monicModPImage f ∣ f

The monic modular image of a nonzero polynomial divides the input: the image is a unit (inverse-leading-coefficient) scaling.

theorem HexBerlekampZassenhausMathlib.dvd_monicModPImage_of_ne_zero {p : ℕ} [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p} (hf : Hex.DensePoly.isZero f = false) : f ∣ monicModPImage f

A nonzero polynomial divides its monic modular image, the reverse direction of monicModPImage_dvd_self_of_ne_zero: the two are associates.

theorem HexBerlekampZassenhausMathlib.modP_mul (p : ℕ) [Hex.ZMod64.Bounds p] (f g : Hex.ZPoly) : Hex.ZPoly.modP p (f * g) = Hex.ZPoly.modP p f * Hex.ZPoly.modP p g

Coefficientwise reduction modulo p preserves multiplication.

theorem HexBerlekampZassenhausMathlib.modP_dvd_modP_of_dvd (p : ℕ) [Hex.ZMod64.Bounds p] {factor core : Hex.ZPoly} (hdvd : factor ∣ core) : Hex.ZPoly.modP p factor ∣ Hex.ZPoly.modP p core

Integer-polynomial divisibility descends through reduction modulo p.

theorem HexBerlekampZassenhausMathlib.monicModPImage_dvd_monicModularImage_of_dvd_of_goodPrime {core factor : Hex.ZPoly} (hdvd : factor ∣ core) (_hcore_ne : core ≠ 0) {primeData : Hex.PrimeChoiceData} (hprime : Hex.Nat.Prime primeData.p) (hgood : Hex.isGoodPrime core primeData.p = true) : monicModPImage (Hex.ZPoly.modP primeData.p factor) ∣ Hex.monicModularImage (Hex.ZPoly.modP primeData.p core)

At a good prime, divisibility survives after normalizing both modular images to monic form.

def HexBerlekampZassenhausMathlib.RepresentsIntegerFactorModP (primeData : Hex.PrimeChoiceData) (factor : Hex.ZPoly) (S : ModPFactorSubset primeData) : Prop

An integer factor is represented modulo the selected prime by a subset of the recorded modular factors when the subset product is the monic modular image of that integer factor.

Equations

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

structure HexBerlekampZassenhausMathlib.ModPSubsetPartitionHypotheses (core : Hex.ZPoly) (primeData : Hex.PrimeChoiceData) (admissiblePrime squareFreeReduction : Prop) : Prop

Proof-facing package for the mod-p irreducible-factor subset partition over the executable PrimeChoiceData surface.

The proposition parameters are hooks for the eventual admissible-prime and square-free-reduction hypotheses. Downstream callers should depend on the existence and uniqueness projections below rather than on a particular analytic proof of this package.

• fModP_eq : primeData.fModP = Hex.ZPoly.modP primeData.p core

  The cached polynomial is the reduction of the integer polynomial.

• admissible_prime : admissiblePrime

  The selected prime satisfies the caller's admissibility condition.

• square_free_reduction : squareFreeReduction

  Reduction modulo the selected prime preserves square-freeness.

• factors_irreducible (i : ModPFactorIndex primeData) : Irreducible (HexPolyFpMathlib.toMathlibPolynomial (modPFactor primeData i))

  Every indexed modular factor is irreducible.

• exists_subset {factor : Hex.ZPoly} : Irreducible (HexPolyZMathlib.toPolynomial factor) → factor ∣ core → ∃ (S : ModPFactorSubset primeData), RepresentsIntegerFactorModP primeData factor S

  Every irreducible integer divisor has a representing modular subset.

• unique_subset {factor : Hex.ZPoly} {S T : ModPFactorSubset primeData} : Irreducible (HexPolyZMathlib.toPolynomial factor) → factor ∣ core → RepresentsIntegerFactorModP primeData factor S → RepresentsIntegerFactorModP primeData factor T → S = T

  The modular subset representing an irreducible integer divisor is unique.

theorem HexBerlekampZassenhausMathlib.existsUnique_modPFactorSubset_of_modPSubsetPartition {core : Hex.ZPoly} {primeData : Hex.PrimeChoiceData} {admissiblePrime squareFreeReduction : Prop} (h : ModPSubsetPartitionHypotheses core primeData admissiblePrime squareFreeReduction) {factor : Hex.ZPoly} (hirr : Irreducible (HexPolyZMathlib.toPolynomial factor)) (hdvd : factor ∣ core) : ∃! S : ModPFactorSubset primeData, RepresentsIntegerFactorModP primeData factor S

Caller-facing mod-p subset partition: an irreducible integer factor of the square-free part has a unique representing subset of the selected modular factors.

theorem HexBerlekampZassenhausMathlib.exists_modPFactorSubset_of_modPSubsetPartition {core : Hex.ZPoly} {primeData : Hex.PrimeChoiceData} {admissiblePrime squareFreeReduction : Prop} (h : ModPSubsetPartitionHypotheses core primeData admissiblePrime squareFreeReduction) {factor : Hex.ZPoly} (hirr : Irreducible (HexPolyZMathlib.toPolynomial factor)) (hdvd : factor ∣ core) : ∃ (S : ModPFactorSubset primeData), RepresentsIntegerFactorModP primeData factor S

Existence projection from the mod-p subset-partition package.

theorem HexBerlekampZassenhausMathlib.unique_modPFactorSubset_of_modPSubsetPartition {core : Hex.ZPoly} {primeData : Hex.PrimeChoiceData} {admissiblePrime squareFreeReduction : Prop} (h : ModPSubsetPartitionHypotheses core primeData admissiblePrime squareFreeReduction) {factor : Hex.ZPoly} {S T : ModPFactorSubset primeData} (hirr : Irreducible (HexPolyZMathlib.toPolynomial factor)) (hdvd : factor ∣ core) (hS : RepresentsIntegerFactorModP primeData factor S) (hT : RepresentsIntegerFactorModP primeData factor T) : S = T

Uniqueness projection from the mod-p subset-partition package.

theorem HexBerlekampZassenhausMathlib.modPFactor_irreducible_of_modPSubsetPartition {core : Hex.ZPoly} {primeData : Hex.PrimeChoiceData} {admissiblePrime squareFreeReduction : Prop} (h : ModPSubsetPartitionHypotheses core primeData admissiblePrime squareFreeReduction) (i : ModPFactorIndex primeData) : Irreducible (HexPolyFpMathlib.toMathlibPolynomial (modPFactor primeData i))

Irreducibility projection for a selected modular factor.

theorem HexBerlekampZassenhausMathlib.mem_modPSubset_of_dvd {core factor : Hex.ZPoly} {primeData : Hex.PrimeChoiceData} {admissiblePrime squareFreeReduction : Prop} (hprime : Nat.Prime primeData.p) (hpart : ModPSubsetPartitionHypotheses core primeData admissiblePrime squareFreeReduction) (hf_inj : Function.Injective fun (i : ModPFactorIndex primeData) => HexPolyFpMathlib.toMathlibPolynomial (modPFactor primeData i)) (hmonic : ∀ (i : ModPFactorIndex primeData), (HexPolyFpMathlib.toMathlibPolynomial (modPFactor primeData i)).Monic) {S : ModPFactorSubset primeData} {i : ModPFactorIndex primeData} (hS : RepresentsIntegerFactorModP primeData factor S) (hdvd : HexPolyFpMathlib.toMathlibPolynomial (modPFactor primeData i) ∣ HexPolyFpMathlib.toMathlibPolynomial (monicModPImage (Hex.ZPoly.modP primeData.p factor))) : i ∈ S

If a selected modular factor divides the Mathlib image of a represented integer-factor product, then its index belongs to the representing subset.

theorem HexBerlekampZassenhausMathlib.natPrime_of_hexNatPrime {p : ℕ} (hp : Hex.Nat.Prime p) : Nat.Prime p

The project-local primality predicate implies Mathlib's Nat.Prime.

theorem HexBerlekampZassenhausMathlib.monicModPImage_scale {p : ℕ} [Hex.ZMod64.Bounds p] (hprime : Hex.Nat.Prime p) {c : Hex.ZMod64 p} (hc : c ≠ 0) (f : Hex.FpPoly p) : monicModPImage (Hex.DensePoly.scale c f) = monicModPImage f

Unit-invariance of monicModPImage. Scaling a modular polynomial by a nonzero residue (a unit modulo a prime) leaves its monic image unchanged: the leading-coefficient normalisation divides the unit scalar back out.

theorem HexBerlekampZassenhausMathlib.monicModPImage_modP_eq_of_associated {p : ℕ} [Hex.ZMod64.Bounds p] (hprime : Hex.Nat.Prime p) {f g : Hex.ZPoly} (hassoc : Associated (HexPolyZMathlib.toPolynomial f) (HexPolyZMathlib.toPolynomial g)) : monicModPImage (Hex.ZPoly.modP p f) = monicModPImage (Hex.ZPoly.modP p g)

Associated factors share a monic modular image. If two integer factors are associated in Polynomial ℤ, their reductions modulo p have the same monic image, because monicModPImage absorbs the unit ±1.

theorem HexBerlekampZassenhausMathlib.representsIntegerFactorModP_of_associated {primeData : Hex.PrimeChoiceData} (hprime : Hex.Nat.Prime primeData.p) {f g : Hex.ZPoly} {S : ModPFactorSubset primeData} (hassoc : Associated (HexPolyZMathlib.toPolynomial f) (HexPolyZMathlib.toPolynomial g)) (hf : RepresentsIntegerFactorModP primeData f S) : RepresentsIntegerFactorModP primeData g S

RepresentsIntegerFactorModP depends only on the Associated class of the integer factor in Polynomial ℤ: a representing subset for f also represents any associate g.

theorem HexBerlekampZassenhausMathlib.unique_modPFactorSubset_up_to_associated {core : Hex.ZPoly} {primeData : Hex.PrimeChoiceData} {admissiblePrime squareFreeReduction : Prop} (hprime : Hex.Nat.Prime primeData.p) (h : ModPSubsetPartitionHypotheses core primeData admissiblePrime squareFreeReduction) {f g : Hex.ZPoly} {S T : ModPFactorSubset primeData} (hg_irr : Irreducible (HexPolyZMathlib.toPolynomial g)) (hg_dvd : g ∣ core) (hS : RepresentsIntegerFactorModP primeData f S) (hT : RepresentsIntegerFactorModP primeData g T) (hassoc : Associated (HexPolyZMathlib.toPolynomial f) (HexPolyZMathlib.toPolynomial g)) : S = T

modP uniqueness up to association. Associated irreducible integer divisors of core have the same representing subset of modular factors, not merely equal ones. Combines unit-invariance of monicModPImage with the package's unique_subset projection.

theorem HexBerlekampZassenhausMathlib.modPFactorSubset_disjoint_of_not_associated {core : Hex.ZPoly} {primeData : Hex.PrimeChoiceData} {admissiblePrime squareFreeReduction : Prop} (hprime : Hex.Nat.Prime primeData.p) (hpart : ModPSubsetPartitionHypotheses core primeData admissiblePrime squareFreeReduction) (hcore_modP_nz : Hex.DensePoly.isZero (Hex.ZPoly.modP primeData.p core) = false) (hsqfree : Squarefree (HexPolyFpMathlib.toMathlibPolynomial (monicModPImage (Hex.ZPoly.modP primeData.p core)))) {f g : Hex.ZPoly} {S T : ModPFactorSubset primeData} (hf_irr : Irreducible (HexPolyZMathlib.toPolynomial f)) (hf_dvd : f ∣ core) (hg_irr : Irreducible (HexPolyZMathlib.toPolynomial g)) (hg_dvd : g ∣ core) (hS : RepresentsIntegerFactorModP primeData f S) (hT : RepresentsIntegerFactorModP primeData g T) (hnotassoc : ¬Associated (HexPolyZMathlib.toPolynomial f) (HexPolyZMathlib.toPolynomial g)) : Disjoint S T

modP pairwise-disjointness. Non-associated irreducible integer divisors of core are represented by disjoint subsets of the modular factors. The genuine square-freeness of the modular reduction is threaded as the explicit hypothesis hsqfree; if two representing subsets shared an index, that modular factor would square-divide the (square-free) modular polynomial, an impossibility.