theorem HexBerlekampZassenhausMathlib.natDegree_toPolynomial_le_degree_getD_of_dvd (f g : Hex.ZPoly) (hf : f ≠ 0) (hgf : g ∣ f) : (HexPolyZMathlib.toPolynomial g).natDegree ≤ Hex.DensePoly.natDegree f

The transported degree of an executable divisor is bounded by the executable degree of the ambient nonzero polynomial.

theorem HexBerlekampZassenhausMathlib.l2norm_toPolynomial_le_coeffL2NormBound (f : Hex.ZPoly) : HexPolyZMathlib.l2norm (HexPolyZMathlib.toPolynomial f) ≤ ↑f.coeffL2NormBound

The executable natural L2 bound dominates the real coefficient-vector norm used by the Mathlib Mignotte theorem.

theorem HexBerlekampZassenhausMathlib.defaultFactorCoeffBound_valid (f : Hex.ZPoly) (hf : f ≠ 0) (g : Hex.ZPoly) : g ∣ f → ∀ (i : ℕ), (Hex.DensePoly.coeff g i).natAbs ≤ f.defaultFactorCoeffBound

The default executable factorization bound is strong enough for every coefficient of every executable divisor of a nonzero input.

theorem HexBerlekampZassenhausMathlib.cofactorCoeff_le_defaultBound (core factor cofactor : Hex.ZPoly) (hcore_ne : core ≠ 0) (hproduct : factor * cofactor = core) (i : ℕ) : ((Hex.DensePoly.scale (Hex.DensePoly.leadingCoeff cofactor) factor).coeff i).natAbs ≤ core.defaultFactorCoeffBound

The default recovery window also bounds the proportional factor reconstructed by the direct-coordinate Hensel path.

When factor * cofactor = core, direct recombination reconstructs leadingCoeff cofactor • factor. The sharpened Mignotte inequality bounds this polynomial by the same executable window as an ordinary divisor; no leading-coefficient multiplier or squared bound is needed.

theorem HexBerlekampZassenhausMathlib.defaultFactorCoeffBound_leadingCoeff_natAbs_le {f : Hex.ZPoly} (hf : f ≠ 0) : (Hex.DensePoly.leadingCoeff f).natAbs ≤ f.defaultFactorCoeffBound

The default factor coefficient bound dominates the natural absolute value of the leading coefficient of any nonzero executable polynomial. Standard packaging of defaultFactorCoeffBound_valid at g := f, hgf := f ∣ f, i := f.size - 1 paired with leadingCoeff_eq_coeff_last.

theorem HexBerlekampZassenhausMathlib.zpoly_ne_zero_of_pos_lc {f : Hex.ZPoly} (hpos : 0 < Hex.DensePoly.leadingCoeff f) : f ≠ 0

A polynomial with positive leading coefficient is nonzero.