theorem
HexBerlekampZassenhausMathlib.findDirectHead_found_le
(coreLc : ℤ)
(target : Hex.ZPoly)
(basis : Hex.LiftData)
(head : Hex.DirectLiftedIndex basis)
(tail : List (Hex.DirectLiftedIndex basis))
{trueSelected trueRemaining : List (Hex.DirectLiftedIndex basis)}
{trueLevel : ℕ}
(htrueMem : (trueSelected, trueRemaining) ∈ Hex.subsetsOfSizeWithComplement tail trueLevel)
{trueCandidate trueQuotient : Hex.ZPoly}
(htrue : Hex.tryDirectSplit coreLc target basis (head :: trueSelected) = some (trueCandidate, trueQuotient))
(levels : List ℕ)
:
List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) levels →
trueLevel ∈ levels →
∀ (budget candidates : ℕ) (completed : Array ℕ) (split : Hex.DirectSplit basis) (budget' candidates' : ℕ)
(completed' : Array ℕ),
Hex.findDirectHead coreLc target basis head tail levels budget candidates completed = Hex.DirectHeadResult.found split budget' candidates' completed' →
∃ (level : ℕ) (selected : List (Hex.DirectLiftedIndex basis)) (remaining : List (Hex.DirectLiftedIndex basis)),
(selected, remaining) ∈ Hex.subsetsOfSizeWithComplement tail level ∧ split.selected = head :: selected ∧ split.remaining = remaining ∧ Hex.tryDirectSplit coreLc target basis split.selected = some (split.candidate, split.quotient) ∧ level ≤ trueLevel
A successful head search occurs no later than any known successful cardinality level. The proof uses the streaming iterator completeness theorem at that known level; a later result would require that level to have been exhausted, which is impossible.
theorem
HexBerlekampZassenhausMathlib.directCandidatePrefilter_trueSupport
{core target factor quotient : Hex.ZPoly}
{B : ℕ}
{data : Hex.PrimeChoiceData}
(facts : DirectLiftFacts core B data)
(hcore_ne : core ≠ 0)
(hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core)
(htarget_ne : target ≠ 0)
(hprecision : 2 * core.defaultFactorCoeffBound < data.p ^ Hex.precisionForCoeffBound B data.p)
{selected : List (Hex.DirectLiftedIndex (core.directLiftData B data))}
(hnodup : selected.Nodup)
(hcandidate :
directSupportCandidate core B data (modPSubsetOfLiftedSubset data (core.directLiftData B data) ⋯ selected.toFinset) = factor)
(hfactor_irr : Irreducible (HexPolyZMathlib.toPolynomial factor))
(hfactor_dvd : factor ∣ target)
(hproduct : quotient * factor = target)
:
Hex.directCandidatePrefilter (Hex.DensePoly.leadingCoeff core) target
(Hex.LiftModulus.ofNat (Hex.liftModulus (core.directLiftData B data)))
(Hex.directSelectedDegree (core.directLiftData B data) selected)
(Hex.directSelectedTrail (core.directLiftData B data) selected) = true
A true modular support passes both cheap direct-candidate prefilters.
theorem
HexBerlekampZassenhausMathlib.tryDirectSplit_trueSupport
{core target factor quotient : Hex.ZPoly}
{B : ℕ}
{data : Hex.PrimeChoiceData}
(facts : DirectLiftFacts core B data)
(hcore_ne : core ≠ 0)
(hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core)
(htarget_ne : target ≠ 0)
(hprecision : 2 * core.defaultFactorCoeffBound < data.p ^ Hex.precisionForCoeffBound B data.p)
{selected : List (Hex.DirectLiftedIndex (core.directLiftData B data))}
(hnodup : selected.Nodup)
(hcandidate :
directSupportCandidate core B data (modPSubsetOfLiftedSubset data (core.directLiftData B data) ⋯ selected.toFinset) = factor)
(hfactor_irr : Irreducible (HexPolyZMathlib.toPolynomial factor))
(hfactor_dvd : factor ∣ target)
(hfactor_lc_pos : 0 < Hex.DensePoly.leadingCoeff factor)
(hfactor_degree_pos : 0 < Hex.DensePoly.natDegree factor)
(hproduct : quotient * factor = target)
:
Hex.tryDirectSplit (Hex.DensePoly.leadingCoeff core) target (core.directLiftData B data) selected = some (factor, quotient)
A recovered true support reaches the successful exact-division leaf of the executable iterator.
theorem
HexBerlekampZassenhausMathlib.tryDirectSplit_containsSupport
{core target factor candidate quotient : Hex.ZPoly}
{B : ℕ}
{data : Hex.PrimeChoiceData}
{J S : ModPFactorSubset data}
(hpartition : 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)
{selected : List (Hex.DirectLiftedIndex (core.directLiftData B data))}
(hnodup : selected.Nodup)
(htry :
Hex.tryDirectSplit (Hex.DensePoly.leadingCoeff core) target (core.directLiftData B data) selected = some (candidate, quotient))
{i : ModPFactorIndex data}
(hiS : i ∈ S)
(hiSelected : i ∈ modPSubsetOfLiftedSubset data (core.directLiftData B data) ⋯ selected.toFinset)
:
S ⊆ modPSubsetOfLiftedSubset data (core.directLiftData B data) ⋯ selected.toFinset
Any successful indexed split containing the distinguished modular index contains the whole true support of the corresponding irreducible factor.
theorem
HexBerlekampZassenhausMathlib.tryDirectSplit_eqSupport_of_card_le
{core target factor candidate quotient : Hex.ZPoly}
{B : ℕ}
{data : Hex.PrimeChoiceData}
{J S : ModPFactorSubset data}
(hpartition : 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)
{selected : List (Hex.DirectLiftedIndex (core.directLiftData B data))}
(hnodup : selected.Nodup)
(htry :
Hex.tryDirectSplit (Hex.DensePoly.leadingCoeff core) target (core.directLiftData B data) selected = some (candidate, quotient))
{i : ModPFactorIndex data}
(hiS : i ∈ S)
(hiSelected : i ∈ modPSubsetOfLiftedSubset data (core.directLiftData B data) ⋯ selected.toFinset)
(hcard : Finset.card (modPSubsetOfLiftedSubset data (core.directLiftData B data) ⋯ selected.toFinset) ≤ Finset.card S)
:
At or below the true support cardinality, a successful head-containing split is exactly that support.