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

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 : 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 Hex.ZPoly.ceilSqrt applied to 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 the ceiling square root, equality holds; in the non-perfect-square branch, the bound follows from the Newton iterator invariant.

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 Hex.ZPoly.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.

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.

6.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