10.7. Key correctness theorems🔗

Two facts pin down the bound for downstream callers. First, the conservative norm bound's square is at most twice the exact squared norm: a bounded overestimate of the Euclidean norm.

theorem

Hex.ZPoly.coeffL2NormBound_sq_le_two_mul_coeffNormSq (f : Hex.ZPoly) :
  f.coeffL2NormBound ^ 2 ≤ 2 * f.coeffNormSq
Hex.ZPoly.coeffL2NormBound_sq_le_two_mul_coeffNormSq
  (f : Hex.ZPoly) :
  f.coeffL2NormBound ^ 2 ≤
    2 * f.coeffNormSq

The executable Euclidean-norm bound has square at most twice the exact squared coefficient norm.

Second, every individual Mignotte bound within the ambient degree range, and the norm bound itself, is dominated by the single uniform defaultFactorCoeffBound, so a caller can use one bound for all factors.

theorem

Hex.ZPoly.mignotteCoeffBound_le_defaultFactorCoeffBound (f : Hex.ZPoly)
  {k j : Nat} (hk : k ≤ (Hex.DensePoly.degree? f).getD 0) (hj : j ≤ k) :
  f.mignotteCoeffBound k j ≤ f.defaultFactorCoeffBound
Hex.ZPoly.mignotteCoeffBound_le_defaultFactorCoeffBound
  (f : Hex.ZPoly) {k j : Nat}
  (hk :
    k ≤ (Hex.DensePoly.degree? f).getD 0)
  (hj : j ≤ k) :
  f.mignotteCoeffBound k j ≤
    f.defaultFactorCoeffBound

Every executable Mignotte coefficient bound within the ambient degree range is bounded by the default uniform factorization bound.

theorem

Hex.ZPoly.coeffL2NormBound_le_defaultFactorCoeffBound (f : Hex.ZPoly) :
  f.coeffL2NormBound ≤ f.defaultFactorCoeffBound
Hex.ZPoly.coeffL2NormBound_le_defaultFactorCoeffBound
  (f : Hex.ZPoly) :
  f.coeffL2NormBound ≤
    f.defaultFactorCoeffBound

The conservative coefficient-norm bound coeffL2NormBound f is at most the default uniform factor coefficient bound defaultFactorCoeffBound f.

Finally, the uniform bound is strictly positive on any nonzero polynomial, which the factorization driver needs to set a valid precision modulus.

theorem

Hex.ZPoly.defaultFactorCoeffBound_pos_of_ne_zero {f : Hex.ZPoly}
  (hf : f ≠ 0) : 0 < f.defaultFactorCoeffBound
Hex.ZPoly.defaultFactorCoeffBound_pos_of_ne_zero
  {f : Hex.ZPoly} (hf : f ≠ 0) :
  0 < f.defaultFactorCoeffBound

A nonzero integer polynomial has positive uniform default factor coefficient bound.

This is the Mignotte-side fact downstream callers need to derive B ≠ 0 and the precision-modulus invariant 2 ≤ p ^ precisionForCoeffBound B p from f ≠ 0 alone (combined with the standard p ≥ 2 provenance from the selected-prime primality lemma and precisionForCoeffBound_spec).