theorem HexRootsMathlib.coeff_natAbs_le_coeffAbsMax (p : Hex.ZPoly) (i : ℕ) : (Hex.DensePoly.coeff p i).natAbs ≤ p.coeffAbsMax

Every coefficient is bounded by the executable coefficient maximum.

theorem HexRootsMathlib.supNorm_toPolyℂ_le (p : Hex.ZPoly) : (toPolyℂ p).supNorm ≤ ↑p.coeffAbsMax

The sup norm of the complex cast is bounded by the executable coefficient maximum.

theorem HexRootsMathlib.mahlerFactor_le_twoPow (n A : ℕ) : √↑n ^ (n + 2) * (√(↑n + 1) * ↑A) ^ (n - 1) ≤ 2 ^ (((n + 2) * Hex.ceilLog2 n + (n - 1) * Hex.ceilLog2 (n + 1) + 2 * (n - 1) * Hex.ceilLog2 A + 1) / 2)

The exact exponent used by mahlerPrec dominates the analytic coefficient factor in the Mahler separation estimate.

theorem HexRootsMathlib.ne_zero_of_separable {p : Hex.ZPoly} (hsep : (Polynomial.map (Int.castRingHom ℚ) (HexPolyZMathlib.toPolynomial p)).Separable) : p ≠ 0

Separability of the rational cast implies that the executable polynomial is nonzero.

theorem HexRootsMathlib.mahlerPrec_separates (p : Hex.ZPoly) (hp : p ≠ 0) (z₁ z₂ : ℂ) : (toPolyℂ p).IsRoot z₁ → (toPolyℂ p).IsRoot z₂ → z₁ ≠ z₂ → 2 ^ (-↑(Hex.mahlerPrec p)) * (1449 / 1024) < ‖z₁ - z₂‖ / 4

The executable mahlerPrec separates any two distinct complex roots of a nonzero polynomial, including polynomials with repeated factors. The left side is the rational upper bound on the circumscribed-disc radius used by HexRoots.

theorem HexRootsMathlib.DyadicSquare.radius_lt_rootDist {p : Hex.ZPoly} (hp : p ≠ 0) {s : Hex.DyadicSquare} (hprec : ↑(Hex.mahlerPrec p) ≤ s.prec) {z w : ℂ} (hz : (toPolyℂ p).IsRoot z) (hw : (toPolyℂ p).IsRoot w) (hne : z ≠ w) : radius s < ‖z - w‖ / 4

A square at the ambient polynomial's Mahler precision has radius less than one quarter of the distance between any two distinct ambient roots.

theorem HexRootsMathlib.DyadicSquare.root_eq_of_discsMeet {p : Hex.ZPoly} (hp : p ≠ 0) {s t : Hex.DyadicSquare} (hs : ↑(Hex.mahlerPrec p) ≤ s.prec) (ht : ↑(Hex.mahlerPrec p) ≤ t.prec) {z w : ℂ} (hz : (toPolyℂ p).IsRoot z) (hw : (toPolyℂ p).IsRoot w) (hzmem : z ∈ closedDisc s) (hwmem : w ∈ closedDisc t) (hmeet : s.discsMeet t = true) : z = w

Intersecting sufficiently refined discs around roots of one ambient polynomial represent the same root. The two isolations may come from different factors of that polynomial.