10.6. The Mignotte coefficient bound🔗

When an integer polynomial is factored, the coefficients of each factor are bounded a priori by the classical Mignotte bound: a binomial coefficient times the Euclidean norm of the original coefficient vector. HexPolyZ packages the executable pieces of that bound. Because the exact Euclidean norm is irrational in general, the norm is replaced by a conservative integer ceiling-square-root overestimate, so every bound here is an upper bound on the true quantity.

The pieces are an executable binomial coefficient and an integer ceiling square root.

def

Hex.ZPoly.binom (n k : Nat) : Nat
Hex.ZPoly.binom (n k : Nat) : Nat

Executable binomial coefficients for the Mignotte bound.

def

Hex.ZPoly.ceilSqrt (n : Nat) : Nat
Hex.ZPoly.ceilSqrt (n : Nat) : Nat

The least natural number whose square is at least n.

theorem

Hex.ZPoly.le_ceilSqrt_sq (n : Nat) : n ≤ Hex.ZPoly.ceilSqrt n ^ 2
Hex.ZPoly.le_ceilSqrt_sq (n : Nat) :
  n ≤ Hex.ZPoly.ceilSqrt n ^ 2

The square of ceilSqrt n is at least n. This is the executable upper-square bound used by the Mignotte coefficient norm chain: in the perfect-square branch of ceilSqrt, equality holds; in the non-perfect-square branch, the bound follows from the Newton iterator invariant sqrtAux_upper_succ.

From these the coefficient-norm bound and the per-coefficient Mignotte bound are assembled, and a single uniform bound is taken over all candidate factor degrees.

def

Hex.ZPoly.coeffNormSq (f : Hex.ZPoly) : Nat
Hex.ZPoly.coeffNormSq (f : Hex.ZPoly) :
  Nat

The squared Euclidean norm of the coefficient vector of f.

def

Hex.ZPoly.coeffL2NormBound (f : Hex.ZPoly) : Nat
Hex.ZPoly.coeffL2NormBound
  (f : Hex.ZPoly) : Nat

A conservative natural-number upper bound on the Euclidean norm of the coefficient vector of f.

def

Hex.ZPoly.mignotteCoeffBound (f : Hex.ZPoly) (k j : Nat) : Nat
Hex.ZPoly.mignotteCoeffBound
  (f : Hex.ZPoly) (k j : Nat) : Nat

The executable Mignotte bound for the j-th coefficient of a degree-k factor of f, using the conservative coeffL2NormBound.

def

Hex.ZPoly.defaultFactorCoeffBound (f : Hex.ZPoly) : Nat
Hex.ZPoly.defaultFactorCoeffBound
  (f : Hex.ZPoly) : Nat

Uniform executable coefficient bound used by the default integer factorization entry point.

It takes the maximum of the executable Mignotte coefficient bounds over every candidate factor degree up to f.degree?.getD 0 and every coefficient index up to that degree.

10.6.1. Worked example: computing the bound🔗

The block below works over g = 1 + x + x² + x³ + x⁴, computes its coefficient-norm bound, some binomial coefficients, a single Mignotte bound, and the uniform default bound.

open Hex Hex.DensePoly

namespace HexPolyZChapterMignotte

-- g = 1 + x + x² + x³ + x⁴
private def g : ZPoly := ofCoeffs #[1, 1, 1, 1, 1]

-- Squared L2 norm of the coefficient vector is 5, and
-- its conservative integer bound is ceilSqrt 5 = 3.
#guard ZPoly.coeffNormSq g = 5
#guard ZPoly.coeffL2NormBound g = 3

-- Executable binomial coefficients.
#guard ZPoly.binom 4 2 = 6
#guard ZPoly.binom 5 2 = 10

-- Mignotte bound for the j=1 coefficient of a degree-2
-- factor: binom 2 1 * coeffL2NormBound g = 2 * 3.
#guard ZPoly.mignotteCoeffBound g 2 1 = 6

-- The uniform bound maximizes over all factor degrees
-- and coefficient indices up to deg g.
#guard ZPoly.defaultFactorCoeffBound g = 18

end HexPolyZChapterMignotte