theorem
HexBerlekampZassenhausMathlib.degree_pos_of_irreducible_dvd_primitive
{core factor : Hex.ZPoly}
(hcore_prim : core.Primitive)
(hirr : Irreducible (HexPolyZMathlib.toPolynomial factor))
(hdvd : factor ∣ core)
:
An irreducible divisor of a primitive integer polynomial has positive executable degree. Constant irreducibles are excluded by primitivity of the target.
structure
HexBerlekampZassenhausMathlib.DirectSearchInvariant
(core : Hex.ZPoly)
(B : ℕ)
(data : Hex.PrimeChoiceData)
(support : ModPFactorSubset data)
(target : Hex.ZPoly)
(localFactors : List (Hex.DirectLiftedIndex (core.directLiftData B data)))
:
Proof state corresponding to one invocation of searchDirectAux.
The current target is nonzero.
The current target divides the original square-free polynomial.
- partition : DirectSupportPartition core B data support target
The remaining modular indices partition the factors of the target.
- localNodup : localFactors.Nodup
No lifted-factor index occurs twice in the remaining list.
- localSupport : localFactors.toFinset = liftedSubsetOfModPSubset data (core.directLiftData B data) ⋯ support
The remaining list contains exactly the lifted indices of
support.
Instances For
theorem
HexBerlekampZassenhausMathlib.findDirectHead_correct
{core target : Hex.ZPoly}
{B : ℕ}
{data : Hex.PrimeChoiceData}
(hcore_prim : core.Primitive)
(hcore_ne : core ≠ 0)
(hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core)
(hcore_degree_pos : 0 < Hex.DensePoly.natDegree core)
(hval : ModPFactorization core data)
(facts : DirectLiftFacts core B data)
(hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p)
(hrecovery : 2 * core.defaultFactorCoeffBound < data.p ^ Hex.precisionForCoeffBound B data.p)
(hgcd : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1)
{J : ModPFactorSubset data}
{head : Hex.DirectLiftedIndex (core.directLiftData B data)}
{tail : List (Hex.DirectLiftedIndex (core.directLiftData B data))}
(state : DirectSearchInvariant core B data J target (head :: tail))
{budget candidates : ℕ}
{completed : Array ℕ}
{split : Hex.DirectSplit (core.directLiftData B data)}
{budget' candidates' : ℕ}
{completed' : Array ℕ}
(hfind :
Hex.findDirectHead (Hex.DensePoly.leadingCoeff core) target (core.directLiftData B data) head tail
(List.range (tail.length + 1)) budget candidates completed = Hex.DirectHeadResult.found split budget' candidates' completed')
:
∃ (factor : Hex.ZPoly) (S : ModPFactorSubset data),
Irreducible (HexPolyZMathlib.toPolynomial factor) ∧ factor ∣ target ∧ S ⊆ J ∧ RepresentsIntegerFactorModP data factor S ∧ Hex.normalizeFactorSign factor = factor ∧ split.candidate = factor ∧ split.quotient * factor = target ∧ split.selected.toFinset = liftedSubsetOfModPSubset data (core.directLiftData B data) ⋯ S ∧ split.remaining.toFinset = liftedSubsetOfModPSubset data (core.directLiftData B data) ⋯ (J \ S) ∧ split.remaining.Nodup
The accepted head split is precisely the irreducible support containing the head, and its remaining list is the exact support complement.
structure
HexBerlekampZassenhausMathlib.DirectFactorListSpec
(target : Hex.ZPoly)
(factors : List Hex.ZPoly)
:
Semantic contract for a completed direct recursive search.
The returned factors multiply to the target polynomial.
- irreducible (factor : Hex.ZPoly) : factor ∈ factors → Irreducible (HexPolyZMathlib.toPolynomial factor)
Every returned factor is irreducible.
- normalized (factor : Hex.ZPoly) : factor ∈ factors → Hex.normalizeFactorSign factor = factor
Every returned factor uses the chosen sign normalization.
- degreePos (factor : Hex.ZPoly) : factor ∈ factors → 0 < Hex.DensePoly.natDegree factor
Every returned factor has positive degree.
Instances For
theorem
HexBerlekampZassenhausMathlib.searchDirectAux_factored
{core : Hex.ZPoly}
{B : ℕ}
{data : Hex.PrimeChoiceData}
(hcore_prim : core.Primitive)
(hcore_ne : core ≠ 0)
(hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core)
(hcore_degree_pos : 0 < Hex.DensePoly.natDegree core)
(hval : ModPFactorization core data)
(facts : DirectLiftFacts core B data)
(hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p)
(hrecovery : 2 * core.defaultFactorCoeffBound < data.p ^ Hex.precisionForCoeffBound B data.p)
(hgcd : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1)
{fuel : ℕ}
{target : Hex.ZPoly}
{localFactors : List (Hex.DirectLiftedIndex (core.directLiftData B data))}
{budget : ℕ}
{stats : Hex.ClassicalStats}
{factors : List Hex.ZPoly}
{budget' : ℕ}
{stats' : Hex.ClassicalStats}
{J : ModPFactorSubset data}
:
DirectSearchInvariant core B data J target localFactors →
Hex.searchDirectAux (Hex.DensePoly.leadingCoeff core) (core.directLiftData B data) fuel target localFactors budget
stats = Hex.DirectSearchResult.factored factors budget' stats' →
DirectFactorListSpec target factors
Every completed recursive direct search is an irreducible factorization of its current target. A resource decline has no mathematical claim.
theorem
HexBerlekampZassenhausMathlib.searchDirect_factored
{core : Hex.ZPoly}
{B : ℕ}
{data : Hex.PrimeChoiceData}
(hcore_prim : core.Primitive)
(hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core)
(hcore_degree_pos : 0 < Hex.DensePoly.natDegree core)
(hcore_squarefree : Squarefree (HexPolyZMathlib.toPolynomial core))
(hB : B = core.defaultFactorCoeffBound)
(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)
{budget : ℕ}
{stats : Hex.ClassicalStats}
{factors : List Hex.ZPoly}
{budget' : ℕ}
{stats' : Hex.ClassicalStats}
(hrun :
Hex.searchDirect (Hex.DensePoly.leadingCoeff core) core (core.directLiftData B data) budget stats = Hex.DirectSearchResult.factored factors budget' stats')
:
DirectFactorListSpec core factors
End-to-end contract for the public direct search over the one full lifted basis.
theorem
HexBerlekampZassenhausMathlib.validDirectFactors_of_spec
{core : Hex.ZPoly}
{factors : List Hex.ZPoly}
(hcore_degree_pos : 0 < Hex.DensePoly.natDegree core)
(h : DirectFactorListSpec core factors)
:
The executable validity guard is implied by the proved direct-search contract.
theorem
HexBerlekampZassenhausMathlib.factorDirectCoreOfPlan_factored
(core : Hex.SquareFreeInput)
(modular : Hex.DirectPrimePlan core)
(hplan : Hex.directPrimePlan? core = some modular)
(hcore_prim : core.poly.Primitive)
(hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core.poly)
(hcore_degree_pos : 0 < Hex.DensePoly.natDegree core.poly)
(hcore_squarefree : Squarefree (HexPolyZMathlib.toPolynomial core.poly))
{budget : ℕ}
{factors : Array Hex.ZPoly}
{stats : Hex.ClassicalStats}
(hrun : Hex.factorDirectCoreOfPlan core modular budget = Hex.ClassicalOutcome.factored factors stats)
:
DirectFactorListSpec core.poly factors.toList
A successful run from a selected direct prime is an irreducible factorization of its indexed direct-coordinate polynomial.
theorem
HexBerlekampZassenhausMathlib.factorDirectCore_factored
(core : Hex.SquareFreeInput)
(hcore_prim : core.poly.Primitive)
(hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core.poly)
(hcore_degree_pos : 0 < Hex.DensePoly.natDegree core.poly)
(hcore_squarefree : Squarefree (HexPolyZMathlib.toPolynomial core.poly))
{budget : ℕ}
{factors : Array Hex.ZPoly}
{stats : Hex.ClassicalStats}
(hrun : Hex.factorDirectCore core budget = Hex.ClassicalOutcome.factored factors stats)
:
DirectFactorListSpec core.poly factors.toList
A successful run of the sole classical engine is an irreducible factorization of its indexed direct-coordinate polynomial.