9.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.Nat.binom (n k : ℕ) : ℕ
Hex.Nat.binom (n k : ℕ) : ℕ

Linear-time binomial coefficient.

Hex.Nat.binom walks a single Pascal row from choose n 0 = 1 using the multiplicative recurrence Hex.Nat.succ_mul_choose_succ, folding over the shorter half min k (n - k) of the row using Hex.Nat.choose_symm. It therefore costs O(min k (n - k)) natural-number operations. The proof-facing Hex.Nat.choose is the exponential Pascal recursion; the forward correctness theorem binom_eq_choose, registered with @[csimp], makes compiled callers use this linear fold.

def

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

Compatibility name for the arithmetic ceiling square root.

theorem

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

The ceiling square root has square at least its argument.

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) : ℕ
Hex.ZPoly.coeffNormSq (f : Hex.ZPoly) : ℕ

The squared Euclidean norm of the coefficient vector of f.

def

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

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 : ℕ) : ℕ
Hex.ZPoly.mignotteCoeffBound
  (f : Hex.ZPoly) (k j : ℕ) : ℕ

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

def

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

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.natDegree and every coefficient index up to that degree.

The compiled runtime uses the value-equal closed form below, registered through @[csimp], which computes the loop-invariant Hex.ZPoly.coeffL2NormBound once instead of recomputing the whole bignum coefficient norm inside every one of the O(deg^2) mignotteCoeffBound terms.

9.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 := #p[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 Nat.binom 4 2 = 6
#guard Nat.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