theorem HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.Worklist.region (work : Array Hex.Component) : Set ℂ

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

Equations

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

theorem HexRootsTheory.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 HexRootsTheory.Results.region {p : Hex.ZPoly} (rs : Array (Hex.Certified p)) : Set ℂ

Union of the semantic regions of an array of certificates.

Equations

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

def HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexNumberFieldTheory.

theorem HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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 HexRootsTheory.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.