theorem HexRootsMathlib.Certified.region_subset_closedDisc {p : Hex.ZPoly} (r : Hex.Certified p) : region r ⊆ DyadicSquare.closedDisc r.square

A certificate's selected region lies in its stored square's closed circumscribed disc.

theorem HexRootsMathlib.isolateAll_loop {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hrun : Hex.isolateAll? p target work strategy = some rs) : ∃ (fuel : ℕ), Hex.isolateLoop p target strategy fuel work = some rs

isolateAll? is the shared loop at its executable fuel value.

theorem HexRootsMathlib.isolateAll_covers {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hrun : Hex.isolateAll? p target work strategy = some rs) {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hz : z ∈ Worklist.region work) : z ∈ Results.region rs

Successful general isolation preserves every polynomial root covered by its starting worklist.

theorem HexRootsMathlib.isolateAll_sound {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hrun : Hex.isolateAll? p target work strategy = some rs) : (∀ r ∈ rs.toList, target ≤ r.square.prec ∧ Certified.Sound r) ∧ ∀ {i j : ℕ} (hi : i < rs.size) (hj : j < rs.size), i ≠ j → Disjoint (DyadicSquare.closedDisc rs[i].square) (DyadicSquare.closedDisc rs[j].square)

Every emitted result meets the target, carries its full semantic count, and distinct indices have disjoint closed circumscribed discs.

theorem HexRootsMathlib.isolateAll_cauchy_covers (p : Hex.ZPoly) (hdegree : 0 < Hex.DensePoly.natDegree p) {target : ℤ} {strategy : Hex.AtomStrategy} {rs : Array (Hex.Certified p)} (hrun : Hex.isolateAll? p target #[Hex.Component.cauchy p hdegree] strategy = some rs) {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) : z ∈ Results.region rs

Starting from the Cauchy component, successful isolation with any strategy covers every complex root.

theorem HexRootsMathlib.isolateAll_covers_once (p : Hex.ZPoly) (hdegree : 0 < Hex.DensePoly.natDegree p) {target : ℤ} {strategy : Hex.AtomStrategy} {rs : Array (Hex.Certified p)} (hrun : Hex.isolateAll? p target #[Hex.Component.cauchy p hdegree] strategy = some rs) {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) : ∃! i : Fin rs.size, z ∈ Certified.region rs[i]

Every complex root belongs to exactly one selected result region in a successful Cauchy-started run. This remains valid when results include Pellet clusters: uniqueness is between certificates, not between roots inside one cluster.

theorem HexRootsMathlib.isolateAll_count (p : Hex.ZPoly) (hdegree : 0 < Hex.DensePoly.natDegree p) {target : ℤ} {strategy : Hex.AtomStrategy} {rs : Array (Hex.Certified p)} (hrun : Hex.isolateAll? p target #[Hex.Component.cauchy p hdegree] strategy = some rs) : ∑ i : Fin rs.size, Certified.count rs[i] = (toPolyℂ p).natDegree

In a successful Cauchy-started run, the sum of the emitted certificate counts is exactly the polynomial degree. Counts are with multiplicity, so a Pellet cluster contributes its stored k, while an atom contributes one.