def Hex.ZPoly.floorSqrt (n : Nat) : Nat

The floor of the square root of n.

Equations

• Hex.ZPoly.floorSqrt n = if n = 0 then 0 else Hex.ZPoly.sqrtAux✝ n (2 * n.log2 + 1) n

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

The least natural number whose square is at least n.

Equations

• Hex.ZPoly.ceilSqrt n = if Hex.ZPoly.floorSqrt n * Hex.ZPoly.floorSqrt n = n then Hex.ZPoly.floorSqrt n else Hex.ZPoly.floorSqrt n + 1

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

The squared Euclidean norm of the coefficient vector of f.

Equations

• f.coeffNormSq = List.foldl (fun (acc i : Nat) => acc + (Hex.DensePoly.coeff f i).natAbs ^ 2) 0 (List.range (Hex.DensePoly.size f))

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

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

Equations

• f.coeffL2NormBound = Hex.ZPoly.ceilSqrt f.coeffNormSq

def Hex.ZPoly.mignotteCoeffBound (f : 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.

Equations

• f.mignotteCoeffBound k j = Hex.Nat.binom k j * f.coeffL2NormBound

noncomputable def Hex.ZPoly.defaultFactorCoeffBound (f : 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.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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Hex.ZPoly.floorSqrt_zero : floorSqrt 0 = 0

Base case of floorSqrt: the n = 0 guard fires before the Newton iteration, so floorSqrt 0 normalizes to 0.

theorem Hex.ZPoly.floorSqrt_sq_le (n : Nat) : floorSqrt n * floorSqrt n ≤ n

The square of floorSqrt n is at most n: it is a lower square root.

@[simp]

theorem Hex.ZPoly.ceilSqrt_zero : ceilSqrt 0 = 0

Base case of ceilSqrt: since floorSqrt 0 = 0 is a perfect square, ceilSqrt returns its floor branch, normalizing ceilSqrt 0 to 0.

theorem Hex.ZPoly.le_ceilSqrt_sq (n : Nat) : n ≤ 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.

theorem Hex.ZPoly.coeffNormSq_eq_sum (f : ZPoly) : f.coeffNormSq = List.foldl (fun (acc i : Nat) => acc + (DensePoly.coeff f i).natAbs ^ 2) 0 (List.range (DensePoly.size f))

Restates coeffNormSq f as the explicit foldl summing (f.coeff i).natAbs ^ 2 over the stored coefficient indices i < f.size.

theorem Hex.ZPoly.coeffL2NormBound_eq_ceilSqrt_coeffNormSq (f : ZPoly) : f.coeffL2NormBound = ceilSqrt f.coeffNormSq

coeffL2NormBound f equals the ceiling square root of the squared coefficient norm coeffNormSq f.

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

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

theorem Hex.ZPoly.mignotteCoeffBound_eq (f : ZPoly) (k j : Nat) : f.mignotteCoeffBound k j = Nat.binom k j * f.coeffL2NormBound

mignotteCoeffBound f k j equals the product binom k j * coeffL2NormBound f of the binomial coefficient and the conservative coefficient-norm bound.

theorem Hex.ZPoly.defaultFactorCoeffBound_eq (f : ZPoly) : f.defaultFactorCoeffBound = have degreeBound := DensePoly.natDegree f; List.foldl (fun (acc k : Nat) => List.foldl (fun (acc j : Nat) => max acc (f.mignotteCoeffBound k j)) acc (List.range (k + 1))) 0 (List.range (degreeBound + 1))

Restates defaultFactorCoeffBound f as the nested foldl taking the maximum of mignotteCoeffBound f k j over factor degrees k up to f.natDegree and coefficient indices j up to k.

@[simp]

theorem Hex.ZPoly.coeffNormSq_zero : coeffNormSq 0 = 0

The zero polynomial has no stored coefficients, so the empty foldl defining coeffNormSq normalizes coeffNormSq 0 to 0.

@[simp]

theorem Hex.ZPoly.coeffL2NormBound_zero : coeffL2NormBound 0 = 0

Base case of the coefficient-norm bound: coeffNormSq 0 = 0 and ceilSqrt 0 = 0, so coeffL2NormBound 0 normalizes to 0.

@[simp]

theorem Hex.ZPoly.mignotteCoeffBound_zero (k j : Nat) : mignotteCoeffBound 0 k j = 0

Base case of the Mignotte coefficient bound: the conservative norm factor coeffL2NormBound 0 = 0 annihilates the product, so mignotteCoeffBound 0 k j normalizes to 0 for every degree k and index j.

@[simp]

theorem Hex.ZPoly.defaultFactorCoeffBound_zero : defaultFactorCoeffBound 0 = 0

Base case of the default factor coefficient bound: every entry of the nested maximum is mignotteCoeffBound 0 k j = 0, so defaultFactorCoeffBound 0 normalizes to 0.

theorem Hex.ZPoly.mignotteCoeffBound_eq_zero_of_lt (f : ZPoly) (k j : Nat) (h : k < j) : f.mignotteCoeffBound k j = 0

The executable Mignotte coefficient bound mignotteCoeffBound f k j vanishes when the coefficient index j exceeds the factor degree k.

theorem Hex.ZPoly.mignotteCoeffBound_le_defaultFactorCoeffBound (f : ZPoly) {k j : Nat} (hk : k ≤ DensePoly.natDegree f) (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 : ZPoly) : f.coeffL2NormBound ≤ f.defaultFactorCoeffBound

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

theorem Hex.ZPoly.defaultFactorCoeffBound_le (f : ZPoly) {B : Nat} (h : ∀ (k : Nat), k ≤ DensePoly.natDegree f → ∀ (j : Nat), j ≤ k → f.mignotteCoeffBound k j ≤ B) : f.defaultFactorCoeffBound ≤ B

Upper-bound companion of mignotteCoeffBound_le_defaultFactorCoeffBound: if every executable Mignotte coefficient bound within the ambient degree range is at most B, then so is the default uniform factor coefficient bound.

theorem Hex.ZPoly.coeffNormSq_pos_of_ne_zero {f : ZPoly} (hf : f ≠ 0) : 0 < f.coeffNormSq

A nonzero integer polynomial has positive squared Euclidean coefficient norm: the last stored coefficient is nonzero and contributes a positive summand to the fold.

theorem Hex.ZPoly.coeffL2NormBound_pos_of_ne_zero {f : ZPoly} (hf : f ≠ 0) : 0 < f.coeffL2NormBound

A nonzero integer polynomial has positive conservative Euclidean coefficient-norm upper bound.

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

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

Consequently, f ≠ 0 gives B ≠ 0; together with p ≥ 2, it also gives the precision-modulus lower bound required by coefficient reconstruction.

theorem Hex.ZPoly.binom_le_central {n k j : Nat} (hjk : j ≤ k) (hkn : k ≤ n) : Nat.binom k j ≤ Nat.binom n (n / 2)

The binomial coefficient over the factor rectangle j ≤ k ≤ n is dominated by the central binomial of the top row: binom k j ≤ binom n (n / 2). This is the monotonicity that collapses the defaultFactorCoeffBound double max.

def Hex.ZPoly.defaultFactorCoeffBoundImpl (f : ZPoly) : Nat

Runtime implementation of defaultFactorCoeffBound: the closed-form central binomial times the single loop-invariant norm.

Equations

• f.defaultFactorCoeffBoundImpl = Hex.Nat.binom (Hex.DensePoly.natDegree f) (Hex.DensePoly.natDegree f / 2) * f.coeffL2NormBound

@[csimp]

theorem Hex.ZPoly.defaultFactorCoeffBound_eq_impl : defaultFactorCoeffBound = defaultFactorCoeffBoundImpl

Register the value-equal closed form defaultFactorCoeffBoundImpl as the compiled implementation of defaultFactorCoeffBound. The @[csimp] swap is backed by the proof, so the runtime one-norm/one-binomial evaluation is verified equal to the O(deg^2) specification.