def HexRootsMathlib.CoversRoots (p : Hex.ZPoly) (squares : Array Hex.DyadicSquare) : Prop

Every complex root lies in one of the retained squares.

Equations

• HexRootsMathlib.CoversRoots p squares = ∀ (z : ℂ), (HexRootsMathlib.toPolyℂ p).IsRoot z → ∃ s ∈ squares.toList, z ∈ HexRootsMathlib.DyadicSquare.closedSquare s

theorem HexRootsMathlib.DyadicSquare.encSquare_prec_of_near {squares : Array Hex.DyadicSquare} {z : ℂ} {prec : ℤ} (hne : 0 < squares.size) (hprec : ∀ s ∈ squares.toList, s.prec = prec) (hnear : ∀ s ∈ squares.toList, ‖z - center s‖ ≤ 65 / 32 * Dyadic.toReal s.radiusHi) : prec - 2 ≤ (Hex.encSquare squares).prec

A component whose common-precision centres satisfy the sharp survivor bound loses at most two precision levels when passed to encSquare.

theorem HexRootsMathlib.encSquare_prec_of_glueCovered {p : Hex.ZPoly} {squares component : Array Hex.DyadicSquare} {prec : ℤ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hdepth : ↑(Hex.separationDepth p) ≤ prec) (hprec : ∀ u ∈ squares.toList, u.prec = prec) (hkeep : ∀ u ∈ squares.toList, Hex.rootFree p u ≠ true) (hc : component ∈ (Hex.glueCovered squares).toList) : prec - 2 ≤ (Hex.encSquare component).prec

The enclosing square of an actual retained glued component loses at most two levels relative to its common leaf precision.

theorem HexRootsMathlib.exists_root_mem_glueCovered {p : Hex.ZPoly} {squares component : Array Hex.DyadicSquare} {prec : ℤ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hdepth : ↑(Hex.separationDepth p) ≤ prec) (hprec : ∀ u ∈ squares.toList, u.prec = prec) (hkeep : ∀ u ∈ squares.toList, Hex.rootFree p u ≠ true) (hcover : CoversRoots p squares) (hc : component ∈ (Hex.glueCovered squares).toList) : ∃ (z : ℂ), (toPolyℂ p).IsRoot z ∧ z ∈ Component.region { squares := component, candidateK := 1 }

At separation depth, global coverage and maximal geometric gluing turn root association into actual root containment: every output component contains the root associated with its retained squares.

theorem HexRootsMathlib.certify_nk_of_glueCovered {p : Hex.ZPoly} {squares component : Array Hex.DyadicSquare} {candidateK : ℕ} {prec : ℤ} {z : ℂ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hdepth : ↑(Hex.separationDepth p) + 3 ≤ prec) (hprec : ∀ u ∈ squares.toList, u.prec = prec) (hkeep : ∀ u ∈ squares.toList, Hex.rootFree p u ≠ true) (hc : component ∈ (Hex.glueCovered squares).toList) (hz : (toPolyℂ p).IsRoot z) (hzcomponent : z ∈ Component.region { squares := component, candidateK := candidateK }) : ∃ (r : Hex.Certified p), Hex.Component.certify? p Hex.AtomStrategy.nk { squares := component, candidateK := candidateK } = some r ∧ z ∈ Certified.region r

A root-bearing component produced by the actual survivor/glue pipeline passes the executable NK certifier three levels after separationDepth.

The three levels are exactly the two-level encSquare loss proved above and the further one-level loss from the doubled square used by certify?. Root membership is a separate loop invariant: proximity of every retained square to some root is used only to bound the component's extent.

theorem HexRootsMathlib.certify_mixed_of_glueCovered {p : Hex.ZPoly} {squares component : Array Hex.DyadicSquare} {candidateK : ℕ} {prec : ℤ} {z : ℂ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hdepth : ↑(Hex.separationDepth p) + 3 ≤ prec) (hprec : ∀ u ∈ squares.toList, u.prec = prec) (hkeep : ∀ u ∈ squares.toList, Hex.rootFree p u ≠ true) (hc : component ∈ (Hex.glueCovered squares).toList) (hz : (toPolyℂ p).IsRoot z) (hzcomponent : z ∈ Component.region { squares := component, candidateK := candidateK }) : ∃ (r : Hex.Certified p), Hex.Component.certify? p Hex.AtomStrategy.nkThenPellet { squares := component, candidateK := candidateK } = some r ∧ z ∈ Certified.region r

The default mixed certifier inherits the same root-bearing survivor guarantee from its NK prefix.