theorem HexBerlekampZassenhausMathlib.normalizeFactorSign_associated (q : Hex.ZPoly) : Associated (HexPolyZMathlib.toPolynomial (Hex.normalizeFactorSign q)) (HexPolyZMathlib.toPolynomial q)

Sign normalization changes an integer polynomial only by a unit.

theorem HexBerlekampZassenhausMathlib.modPFactorSubset_disjoint_of_modPFactorization {core : Hex.ZPoly} {data : Hex.PrimeChoiceData} (hval : ModPFactorization core data) (hcore_pos : 0 < Hex.DensePoly.natDegree core) {f g : Hex.ZPoly} {S T : ModPFactorSubset data} (hf_irr : Irreducible (HexPolyZMathlib.toPolynomial f)) (hf_dvd : f ∣ core) (hg_irr : Irreducible (HexPolyZMathlib.toPolynomial g)) (hg_dvd : g ∣ core) (hS : RepresentsIntegerFactorModP data f S) (hT : RepresentsIntegerFactorModP data g T) (hnotassoc : ¬Associated (HexPolyZMathlib.toPolynomial f) (HexPolyZMathlib.toPolynomial g)) : Disjoint S T

Distinct irreducible integer factors have disjoint direct modular supports at the selected square-free prime.

noncomputable def HexBerlekampZassenhausMathlib.directSupportCandidate (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (S : ModPFactorSubset data) : Hex.ZPoly

The selected direct candidate, expressed on a modular support.

Equations

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

theorem HexBerlekampZassenhausMathlib.leadingCoeff_cast_ne_zero_of_gcd (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (hprime : Hex.Nat.Prime data.p) (hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p) (hgcd : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) : ↑(Hex.DensePoly.leadingCoeff core) ≠ 0

The good-prime leading coefficient remains nonzero in ZMod p, expressed from the stronger precision-level gcd invariant owned by the direct lift.

theorem HexBerlekampZassenhausMathlib.directSupportCandidate_map_associated (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (facts : DirectLiftFacts core B data) (hprime : Hex.Nat.Prime data.p) (hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p) (hgcd : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) (S : ModPFactorSubset data) : let d := core.directLiftData B data; have T := liftedSubsetOfModPSubset data d ⋯ S; Associated (Polynomial.map (Int.castRingHom (ZMod data.p)) (HexPolyZMathlib.toPolynomial (scaledRecombinationCandidate core d T))) (Polynomial.map (Int.castRingHom (ZMod data.p)) (HexPolyZMathlib.toPolynomial (liftedFactorProduct d T)))

Modulo the selected prime, a direct candidate is associated to the product of exactly its selected lifted factors.

The centered lift is congruent to the scaled lifted product. Its content is a unit modulo p because that mapped polynomial is nonzero; primitive-part and sign normalization therefore change it only by units. Finally the leading-coefficient scale is itself a unit.

theorem HexBerlekampZassenhausMathlib.modPSubset_subset_of_product_dvd {core : Hex.ZPoly} {data : Hex.PrimeChoiceData} (hval : ModPFactorization core data) {S T : ModPFactorSubset data} (hdvd : HexPolyFpMathlib.toMathlibPolynomial (modPFactorProduct data S) ∣ HexPolyFpMathlib.toMathlibPolynomial (modPFactorProduct data T)) : S ⊆ T

Divisibility between products of the cached distinct modular factors reflects subset containment.

theorem HexBerlekampZassenhausMathlib.directSupport_subset_of_dvd {core factor : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} (hval : ModPFactorization core data) (facts : DirectLiftFacts core B data) (hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p) (hgcd : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) {S T : ModPFactorSubset data} (hrecover : directSupportCandidate core B data S = factor) (hdvd : factor ∣ directSupportCandidate core B data T) : S ⊆ T

Structural support containment for the direct candidate.

theorem HexBerlekampZassenhausMathlib.leadingCoeff_pos_of_normalized {f : Hex.ZPoly} (hf : f ≠ 0) (hnorm : Hex.normalizeFactorSign f = f) : 0 < Hex.DensePoly.leadingCoeff f

A normalized nonzero integer polynomial has positive leading coefficient.

theorem HexBerlekampZassenhausMathlib.directSupportCandidate_eq_of_irreducible_dvd {core factor : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} (hcore_primitive : core.Primitive) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hrecovery : 2 * core.defaultFactorCoeffBound < data.p ^ Hex.precisionForCoeffBound B data.p) (hval : ModPFactorization core data) (hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p) (hgcd : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) {S : ModPFactorSubset data} (hirr : Irreducible (HexPolyZMathlib.toPolynomial factor)) (hdvd : factor ∣ core) (hnorm : Hex.normalizeFactorSign factor = factor) (hrep : RepresentsIntegerFactorModP data factor S) : directSupportCandidate core B data S = factor

Every normalized irreducible divisor of the primitive direct polynomial is recovered exactly from its unique modular support.

structure HexBerlekampZassenhausMathlib.DirectSupportPartition (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (J : ModPFactorSubset data) (target : Hex.ZPoly) : Prop

The direct support model retained by recursive recombination. Every remaining modular index belongs to exactly one irreducible divisor of the current target, and its direct candidate is that normalized factor.

• targetSquarefree : Squarefree (HexPolyZMathlib.toPolynomial target)

  The current target has no repeated irreducible factors.

• existsSupport {factor : Hex.ZPoly} : Irreducible (HexPolyZMathlib.toPolynomial factor) → factor ∣ target → ∃ S ⊆ J, RepresentsIntegerFactorModP data factor S

  Every irreducible divisor of the target has a support inside J.

• cover {i : ModPFactorIndex data} : i ∈ J → ∃ (factor : Hex.ZPoly) (S : ModPFactorSubset data), Irreducible (HexPolyZMathlib.toPolynomial factor) ∧ factor ∣ target ∧ S ⊆ J ∧ i ∈ S ∧ RepresentsIntegerFactorModP data factor S ∧ Hex.normalizeFactorSign factor = factor ∧ directSupportCandidate core B data S = factor

  Every remaining modular index belongs to a recovered irreducible factor.

• pairwiseDisjoint {f g : Hex.ZPoly} {S T : ModPFactorSubset data} : Irreducible (HexPolyZMathlib.toPolynomial f) → f ∣ target → S ⊆ J → RepresentsIntegerFactorModP data f S → Irreducible (HexPolyZMathlib.toPolynomial g) → g ∣ target → T ⊆ J → RepresentsIntegerFactorModP data g T → ¬Associated (HexPolyZMathlib.toPolynomial f) (HexPolyZMathlib.toPolynomial g) → Disjoint S T

  Nonassociated irreducible factors have disjoint modular supports.

• unique {f g : Hex.ZPoly} {S T : ModPFactorSubset data} : Irreducible (HexPolyZMathlib.toPolynomial f) → f ∣ target → S ⊆ J → RepresentsIntegerFactorModP data f S → Irreducible (HexPolyZMathlib.toPolynomial g) → g ∣ target → T ⊆ J → RepresentsIntegerFactorModP data g T → Associated (HexPolyZMathlib.toPolynomial f) (HexPolyZMathlib.toPolynomial g) → S = T

  Associated irreducible factors have the same modular support.

theorem HexBerlekampZassenhausMathlib.directSupportPartition_initial (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (hcore_primitive : core.Primitive) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hcore_degree_pos : 0 < Hex.DensePoly.natDegree core) (hcore_squarefree : Squarefree (HexPolyZMathlib.toPolynomial core)) (hrecovery : 2 * core.defaultFactorCoeffBound < data.p ^ Hex.precisionForCoeffBound B data.p) (hval : ModPFactorization core data) (hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p) (hgcd : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) : DirectSupportPartition core B data Finset.univ core

Construct the initial direct support partition from the selected cached good-prime factorization.

theorem HexBerlekampZassenhausMathlib.DirectSupportPartition.coverHead {core target : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} {J : ModPFactorSubset data} (h : DirectSupportPartition core B data J target) (head : ModPFactorIndex data) (hhead : head ∈ J) : ∃ (factor : Hex.ZPoly) (S : ModPFactorSubset data), Irreducible (HexPolyZMathlib.toPolynomial factor) ∧ factor ∣ target ∧ S ⊆ J ∧ head ∈ S ∧ RepresentsIntegerFactorModP data factor S ∧ Hex.normalizeFactorSign factor = factor ∧ directSupportCandidate core B data S = factor

The support containing the distinguished head modular factor.

theorem HexBerlekampZassenhausMathlib.DirectSupportPartition.factorDvdCandidate {core target factor : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} {J S T : ModPFactorSubset data} (h : DirectSupportPartition core B data J target) (hval : ModPFactorization core data) (facts : DirectLiftFacts core B data) (hcore_degree_pos : 0 < Hex.DensePoly.natDegree core) (hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p) (hgcd : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) (hfactor_irr : Irreducible (HexPolyZMathlib.toPolynomial factor)) (hfactor_dvd : factor ∣ target) (hSJ : S ⊆ J) (hfactor_rep : RepresentsIntegerFactorModP data factor S) {i : ModPFactorIndex data} (hiS : i ∈ S) (hiT : i ∈ T) (hcandidate_dvd : directSupportCandidate core B data T ∣ target) : factor ∣ directSupportCandidate core B data T

If an accepted direct candidate contains a modular index, then it contains the irreducible integer factor represented by the true support containing that index.

Factor the accepted candidate in ℤ[X]. The distinguished modular prime factor divides its mapped normalized-factor product, so it divides the image of one normalized integer factor. That factor has a support in the direct partition containing the same modular index. Pairwise disjointness forces it to be associated to the distinguished true factor.

theorem HexBerlekampZassenhausMathlib.DirectSupportPartition.supportSubsetCandidate {core target factor : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} {J S T : ModPFactorSubset data} (h : DirectSupportPartition core B data J target) (hval : ModPFactorization core data) (facts : DirectLiftFacts core B data) (hcore_degree_pos : 0 < Hex.DensePoly.natDegree core) (hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p) (hgcd : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) (hfactor_irr : Irreducible (HexPolyZMathlib.toPolynomial factor)) (hfactor_dvd : factor ∣ target) (hSJ : S ⊆ J) (hfactor_rep : RepresentsIntegerFactorModP data factor S) (hrecover : directSupportCandidate core B data S = factor) {i : ModPFactorIndex data} (hiS : i ∈ S) (hiT : i ∈ T) (hcandidate_dvd : directSupportCandidate core B data T ∣ target) : S ⊆ T

The modular support of the distinguished true factor is contained in any accepted direct support containing the distinguished modular index.

theorem HexBerlekampZassenhausMathlib.DirectSupportPartition.remove {core target quotient emitted : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} {J S : ModPFactorSubset data} (h : DirectSupportPartition core B data J target) (hquot : quotient * emitted = target) (hSrep : RepresentsIntegerFactorModP data emitted S) (hSJ : S ⊆ J) (hEmittedIrr : Irreducible (HexPolyZMathlib.toPolynomial emitted)) (hEmittedDvd : emitted ∣ target) : DirectSupportPartition core B data (J \ S) quotient

Remove one emitted irreducible support and transport the partition to the exact quotient without selecting another prime or performing another lift.