theorem HexRootsMathlib.mem_glueCovered {sqs : Array Hex.DyadicSquare} {s : Hex.DyadicSquare} (hs : s ∈ sqs.toList) : ∃ c ∈ (Hex.glueCovered sqs).toList, s ∈ c.toList

Every input square occurs in one of the guarded connected components.

theorem HexRootsMathlib.isRoot_mem_refine1 {p : Hex.ZPoly} {c : Hex.Component} {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hz : z ∈ Component.region c) : ∃ d ∈ (Hex.Component.refine1 p c).toList, z ∈ Component.region d

One guarded subdivision round preserves every polynomial root covered by the input component.

def HexRootsMathlib.Worklist.region (work : Array Hex.Component) : Set ℂ

Union of the closed-square regions retained by a worklist.

Equations

• HexRootsMathlib.Worklist.region work = {z : ℂ | ∃ c ∈ work.toList, z ∈ HexRootsMathlib.Component.region c}

theorem HexRootsMathlib.isRoot_mem_refineAll {p : Hex.ZPoly} {work : Array Hex.Component} {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hz : z ∈ Worklist.region work) : z ∈ Worklist.region (Hex.Component.refineAll p work)

A globally normalized subdivision round preserves every polynomial root covered by its input worklist.

def HexRootsMathlib.Results.region {p : Hex.ZPoly} (rs : Array (Hex.Certified p)) : Set ℂ

Union of the semantic regions of an array of certificates.

Equations

• HexRootsMathlib.Results.region rs = {z : ℂ | ∃ r ∈ rs.toList, z ∈ HexRootsMathlib.Certified.region r}

def HexRootsMathlib.Certifier.Preserves (p : Hex.ZPoly) (strategy : Hex.AtomStrategy) : Prop

Semantic hypothesis consumed by the structural loop proof: every successful certificate covers every polynomial root covered by its input component. The .nk and general certificate developments instantiate this separately. In particular, speculative recentring must use the executable containment and same-count guards; it does not follow from geometric containment of the input component in the returned region.

Equations

• One or more equations did not get rendered due to their size.

theorem HexRootsMathlib.isRoot_mem_next {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} (hcert : Certifier.Preserves p strategy) {work : Array Hex.Component} {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hz : z ∈ Worklist.region work) : z ∈ Worklist.region (Hex.IsolationLoop.next p target (Hex.IsolationLoop.attempts p strategy work))

The non-emitting transition preserves every covered polynomial root.

theorem HexRootsMathlib.isRoot_mem_nextLocal {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} (hcert : Certifier.Preserves p strategy) {work : Array Hex.Component} {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hz : z ∈ Worklist.region work) : z ∈ Worklist.region (Hex.IsolationLoop.nextLocal p target (Hex.IsolationLoop.attempts p strategy work))

The lineage-local transition used by single-atom refinement preserves every covered polynomial root.

theorem HexRootsMathlib.mem_next_of_hold {p : Hex.ZPoly} {target : ℤ} {tried : Array (Hex.Component × Option (Hex.Certified p))} {i : ℕ} (hi : i < tried.size) {c : Hex.Component} {r : Hex.Certified p} (hget : tried[i] = (c, some r)) (hdepth : Hex.IsolationLoop.normalized p target tried = true) (hready : target ≤ r.square.prec) (hdisjoint : Hex.IsolationLoop.overlaps tried i r = false) : c ∈ Hex.IsolationLoop.next p target tried

A target-ready successful attempt whose disc meets no other successful attempt holds its original component in the next worklist.

theorem HexRootsMathlib.mem_next_of_adopt {p : Hex.ZPoly} {target : ℤ} {tried : Array (Hex.Component × Option (Hex.Certified p))} {i : ℕ} (hi : i < tried.size) {c : Hex.Component} {r : Hex.Certified p} (hget : tried[i] = (c, some r)) (hdepth : Hex.IsolationLoop.normalized p target tried = true) (hcontinue : (decide (target ≤ r.square.prec) && !Hex.IsolationLoop.overlaps tried i r) = false) (hfiner : c.prec < r.toComponent.prec) : r.toComponent ∈ Hex.IsolationLoop.next p target tried

A non-held successful attempt whose doubled result is strictly finer re-enters the next worklist as that doubled covering component.

theorem HexRootsMathlib.outputs_ready {p : Hex.ZPoly} {target : ℤ} {tried : Array (Hex.Component × Option (Hex.Certified p))} (hready : Hex.IsolationLoop.allReady target tried = true) (r : Hex.Certified p) : r ∈ (Hex.IsolationLoop.outputs tried).toList → target ≤ r.square.prec

allReady means every emitted certificate meets the target precision.

theorem HexRootsMathlib.isRoot_mem_outputs {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} (hcert : Certifier.Preserves p strategy) {work : Array Hex.Component} {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hz : z ∈ Worklist.region work) (hready : Hex.IsolationLoop.allReady target (Hex.IsolationLoop.attempts p strategy work) = true) : z ∈ Results.region (Hex.IsolationLoop.outputs (Hex.IsolationLoop.attempts p strategy work))

When every attempt succeeds, the emitted certificate regions cover every polynomial root covered by the attempted worklist.

theorem HexRootsMathlib.refineLoop_covers {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} (hcert : Certifier.Preserves p strategy) {fuel : ℕ} {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hloop : Hex.refineLoop p target strategy fuel work = some rs) {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hz : z ∈ Worklist.region work) : z ∈ Results.region rs

Parametric coverage theorem for the single-atom refinement loop.

theorem HexRootsMathlib.refineLoop_ready_disjoint {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} {fuel : ℕ} {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hloop : Hex.refineLoop p target strategy fuel work = some rs) : (∀ r ∈ rs.toList, target ≤ r.square.prec) ∧ Hex.pairwiseDisjoint (Array.map (fun (x : Hex.Certified p) => x.square) rs) = true

A successful one-atom refinement loop meets its target and returns its single atom certificate (hence a pairwise-disjoint result).

theorem HexRootsMathlib.refineFastLoop_covers {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} (hcert : Certifier.Preserves p strategy) {fuel : ℕ} {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hloop : Hex.refineFastLoop p target strategy fuel work = some rs) {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hz : z ∈ Worklist.region work) : z ∈ Results.region rs

Coverage for the bounded lineage-local speculative refinement pass.

theorem HexRootsMathlib.refineFastLoop_ready_disjoint {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} {fuel : ℕ} {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hloop : Hex.refineFastLoop p target strategy fuel work = some rs) : (∀ r ∈ rs.toList, target ≤ r.square.prec) ∧ Hex.pairwiseDisjoint (Array.map (fun (x : Hex.Certified p) => x.square) rs) = true

A successful speculative refinement pass returns its single target-ready atom certificate.

theorem HexRootsMathlib.array_mapM_some_get {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} {ys : Array β} (hmap : Array.mapM f xs = some ys) : xs.size = ys.size ∧ ∀ (i : ℕ) (hi : i < xs.size) (hj : i < ys.size), f xs[i] = some ys[i]

An option-valued array map that succeeds preserves size and maps corresponding entries. Shared plumbing for the isolation-loop soundness proofs here and in NKDriver, Isolate, and HexNumberFieldMathlib.

theorem HexRootsMathlib.refineFastAtom_ready {p : Hex.ZPoly} {iso iso' : Hex.DyadicRootIsolation p} {target : ℤ} {strategy : Hex.AtomStrategy} (hrefine : Hex.refineFastAtom? iso target strategy = some iso') : target ≤ iso'.square.prec

A successful bounded speculative atom refinement reaches the requested precision.

theorem HexRootsMathlib.refineAtom_ready {p : Hex.ZPoly} {iso iso' : Hex.DyadicRootIsolation p} {target : ℤ} {strategy : Hex.AtomStrategy} (hrefine : Hex.refineAtom? iso target strategy = some iso') : target ≤ iso'.square.prec

A successful internal atom refinement reaches the requested precision.

theorem HexRootsMathlib.refineAtom_preserves {p : Hex.ZPoly} {strategy : Hex.AtomStrategy} (hcert : Certifier.Preserves p strategy) {iso iso' : Hex.DyadicRootIsolation p} {target : ℤ} (hrefine : Hex.refineAtom? iso target strategy = some iso') {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hz : z ∈ Certified.region (Hex.Certified.atom iso)) : z ∈ Certified.region (Hex.Certified.atom iso')

Internal atom refinement preserves the atom's semantic root.

theorem HexRootsMathlib.refineFastAtom_preserves {p : Hex.ZPoly} {strategy : Hex.AtomStrategy} (hcert : Certifier.Preserves p strategy) {iso iso' : Hex.DyadicRootIsolation p} {target : ℤ} (hrefine : Hex.refineFastAtom? iso target strategy = some iso') {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hz : z ∈ Certified.region (Hex.Certified.atom iso)) : z ∈ Certified.region (Hex.Certified.atom iso')

The bounded speculative atom refinement preserves the atom's semantic root whenever it succeeds.

theorem HexRootsMathlib.refineAttempt_ready {p : Hex.ZPoly} {t : Hex.Component × Option (Hex.Certified p)} {iso' : Hex.DyadicRootIsolation p} {target : ℤ} {strategy : Hex.AtomStrategy} (hrefine : Hex.IsolationLoop.refineAttempt? target strategy t = some iso') : target ≤ iso'.square.prec

Every successful all-atoms refinement attempt reaches the requested precision.

theorem HexRootsMathlib.refineAttempt_preserves {p : Hex.ZPoly} {c : Hex.Component} {strategy : Hex.AtomStrategy} (hcert : Certifier.Preserves p strategy) {iso iso' : Hex.DyadicRootIsolation p} {target : ℤ} (hrefine : Hex.IsolationLoop.refineAttempt? target strategy (c, some (Hex.Certified.atom iso)) = some iso') {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hz : z ∈ Certified.region (Hex.Certified.atom iso)) : z ∈ Certified.region (Hex.Certified.atom iso')

Refining one successful atom in the all-atoms finisher preserves its semantic root across both the bounded local pass and the complete fallback.

theorem HexRootsMathlib.finishAllAtoms_atoms {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} {tried : Array (Hex.Component × Option (Hex.Certified p))} {rs : Array (Hex.Certified p)} (hfinish : Hex.IsolationLoop.finishAllAtoms? p target strategy tried = some rs) (r : Hex.Certified p) : r ∈ rs.toList → ∃ (iso : Hex.DyadicRootIsolation p), r = Hex.Certified.atom iso

The opportunistic all-atoms fast path returns atoms only.

theorem HexRootsMathlib.finishAllAtoms_ready_disjoint {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} {tried : Array (Hex.Component × Option (Hex.Certified p))} {rs : Array (Hex.Certified p)} (hfinish : Hex.IsolationLoop.finishAllAtoms? p target strategy tried = some rs) : (∀ r ∈ rs.toList, target ≤ r.square.prec) ∧ Hex.pairwiseDisjoint (Array.map (fun (x : Hex.Certified p) => x.square) rs) = true

A successful all-atoms fast path meets the target and returns pairwise disjoint atom discs.

theorem HexRootsMathlib.finishAllAtoms_covers {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} (hcert : Certifier.Preserves p strategy) {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hfinish : Hex.IsolationLoop.finishAllAtoms? p target strategy (Hex.IsolationLoop.attempts p strategy work) = some rs) {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hz : z ∈ Worklist.region work) : z ∈ Results.region rs

The all-atoms fast path preserves every polynomial root covered by its attempted worklist.

theorem HexRootsMathlib.finishAtoms_atoms {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} {tried : Array (Hex.Component × Option (Hex.Certified p))} {rs : Array (Hex.Certified p)} (hfinish : Hex.IsolationLoop.finishAtoms? p target strategy tried = some rs) (r : Hex.Certified p) : r ∈ rs.toList → ∃ (iso : Hex.DyadicRootIsolation p), r = Hex.Certified.atom iso

A successful atom-only finish emits only atom certificates.

theorem HexRootsMathlib.finishAtoms_ready_disjoint {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} {tried : Array (Hex.Component × Option (Hex.Certified p))} {rs : Array (Hex.Certified p)} (hfinish : Hex.IsolationLoop.finishAtoms? p target strategy tried = some rs) : (∀ r ∈ rs.toList, target ≤ r.square.prec) ∧ Hex.pairwiseDisjoint (Array.map (fun (x : Hex.Certified p) => x.square) rs) = true

A successful atom-only finish meets the target precision and emits pairwise-disjoint squares.

theorem HexRootsMathlib.finishAtoms_covers {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} (hcert : Certifier.Preserves p strategy) {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hfinish : Hex.IsolationLoop.finishAtoms? p target strategy (Hex.IsolationLoop.attempts p strategy work) = some rs) {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hz : z ∈ Worklist.region work) : z ∈ Results.region rs

With a preserving certifier, a successful atom-only finish covers every root covered by the input worklist.

theorem HexRootsMathlib.isolateLoop_covers {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} (hcert : Certifier.Preserves p strategy) {fuel : ℕ} {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hloop : Hex.isolateLoop p target strategy fuel work = some rs) {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hz : z ∈ Worklist.region work) : z ∈ Results.region rs

Parametric coverage theorem for the fuel-based isolation loop. No certificate analysis enters: the proof consumes only Certifier.Preserves and follows the executable emitting and non-emitting branches.

theorem HexRootsMathlib.isolateLoop_ready_disjoint {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} {fuel : ℕ} {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hloop : Hex.isolateLoop p target strategy fuel work = some rs) : (∀ r ∈ rs.toList, target ≤ r.square.prec) ∧ Hex.pairwiseDisjoint (Array.map (fun (x : Hex.Certified p) => x.square) rs) = true

Every successful loop result meets the requested precision and passes the executable pairwise-disjoint-disc test.

theorem HexRootsMathlib.isolateLoop_disjoint {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} {fuel : ℕ} {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hloop : Hex.isolateLoop p target strategy fuel work = some rs) {i j : ℕ} (hi : i < rs.size) (hj : j < rs.size) (hij : i < j) : Disjoint (DyadicSquare.closedDisc rs[i].square) (DyadicSquare.closedDisc rs[j].square)

Distinct loop outputs have disjoint closed circumscribed discs.

theorem HexRootsMathlib.isolateLoop_disjoint_of_ne {p : Hex.ZPoly} {target : ℤ} {strategy : Hex.AtomStrategy} {fuel : ℕ} {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hloop : Hex.isolateLoop p target strategy fuel work = some rs) {i j : ℕ} (hi : i < rs.size) (hj : j < rs.size) (hij : i ≠ j) : Disjoint (DyadicSquare.closedDisc rs[i].square) (DyadicSquare.closedDisc rs[j].square)

Any two differently indexed loop outputs have disjoint closed circumscribed discs.