theorem
HexBerlekampZassenhausMathlib.bhksFactors_irreducible_of_count
{core : Hex.ZPoly}
{B : ℕ}
{primeData : Hex.PrimeChoiceData}
{k fuel : ℕ}
{coreFactors : Array Hex.ZPoly}
(hcore_ne : core ≠ 0)
(h : Hex.bhksRecoveryCoreWithBound core B primeData k fuel = some coreFactors)
(hcount :
(List.map HexPolyZMathlib.toPolynomial coreFactors.toList).length = (UniqueFactorizationMonoid.normalizedFactors (HexPolyZMathlib.toPolynomial core)).card)
(factor : Hex.ZPoly)
:
factor ∈ coreFactors.toList → Irreducible (HexPolyZMathlib.toPolynomial factor)
If a verified CLD candidate list has the normalized-factor cardinality, every candidate is irreducible.
theorem
HexBerlekampZassenhausMathlib.bhksRecoveryCoreWithBound_some_factor_count_le
{core : Hex.ZPoly}
{B : ℕ}
{primeData : Hex.PrimeChoiceData}
{k fuel : ℕ}
{coreFactors : Array Hex.ZPoly}
(hcore_ne : core ≠ 0)
(h : Hex.bhksRecoveryCoreWithBound core B primeData k fuel = some coreFactors)
:
A verified CLD candidate list cannot contain more nonunit factors than the normalized factorization of the input.
theorem
HexBerlekampZassenhausMathlib.bhksFactors_zpolyIrreducible_of_count
{core : Hex.ZPoly}
{B : ℕ}
{primeData : Hex.PrimeChoiceData}
{k fuel : ℕ}
{coreFactors : Array Hex.ZPoly}
(hcore_ne : core ≠ 0)
(h : Hex.bhksRecoveryCoreWithBound core B primeData k fuel = some coreFactors)
(hcount :
(List.map HexPolyZMathlib.toPolynomial coreFactors.toList).length = (UniqueFactorizationMonoid.normalizedFactors (HexPolyZMathlib.toPolynomial core)).card)
(factor : Hex.ZPoly)
:
factor ∈ coreFactors.toList → factor.Irreducible
ZPoly form of bhksFactors_irreducible_of_count.