theorem HexRootsMathlib.cauchyBound_le_two_pow (p : Hex.ZPoly) (h : 0 < Hex.DensePoly.natDegree p) : ↑(toPolyℂ p).cauchyBound ≤ 2 ^ Hex.cauchyExp p

The Mathlib Cauchy bound is no larger than the power of two selected by the executable integer calculation.

theorem HexRootsMathlib.isRoot_mem_cauchySquare (p : Hex.ZPoly) (h : 0 < Hex.DensePoly.natDegree p) {z : ℂ} (hz : (toPolyℂ p).IsRoot z) : z ∈ DyadicSquare.closedSquare { re := 0, im := 0, prec := -↑(Hex.cauchyExp p) }

Every root of the complex cast lies in the closed square stored in the executable initial component.

theorem HexRootsMathlib.exists_mem_component_cauchy (p : Hex.ZPoly) (h : 0 < Hex.DensePoly.natDegree p) {z : ℂ} (hz : (toPolyℂ p).IsRoot z) : ∃ s ∈ (Hex.Component.cauchy p h).squares.toList, z ∈ DyadicSquare.closedSquare s

Component-level form of Cauchy coverage: every root occurs in the union of the squares returned by Component.cauchy.