def HexRootsMathlib.Worklist.Within (work : Array Hex.Component) (outer : Hex.DyadicSquare) : Prop

Every worklist square remains inside the starting atom neighborhood.

Equations

• HexRootsMathlib.Worklist.Within work outer = ∀ c ∈ work.toList, ∀ s ∈ c.squares.toList, HexRootsMathlib.DyadicSquare.closedSquare s ⊆ HexRootsMathlib.DyadicSquare.closedSquare outer

theorem HexRootsMathlib.Worklist.refineAll_within {p : Hex.ZPoly} {work : Array Hex.Component} {outer : Hex.DyadicSquare} (hwithin : Within work outer) : Within (Hex.Component.refineAll p work) outer

A globally reglued subdivision round preserves confinement.

theorem HexRootsMathlib.Worklist.refineAll_mem_not_rootFree {p : Hex.ZPoly} {work : Array Hex.Component} {c : Hex.Component} (hc : c ∈ (Hex.Component.refineAll p work).toList) {s : Hex.DyadicSquare} (hs : s ∈ c.squares.toList) : Hex.rootFree p s ≠ true

Every square emitted by refineAll failed the executable T₀ test.

theorem HexRootsMathlib.nearRoot_of_outer {p : Hex.ZPoly} (rep : Hex.RefinedIsolation p) {s : Hex.DyadicSquare} (hprec : ↑(Hex.separationDepth p) ≤ s.prec) (hkeep : Hex.rootFree p s ≠ true) (hwithin : DyadicSquare.closedSquare s ⊆ DyadicSquare.closedSquare (↑rep).square.doubled) : NearRoot p s (RefinedIsolation.root rep)

A retained separation-depth square confined to a refined atom's doubled square has that atom's locally simple root as its sharp nearby root.

theorem HexRootsMathlib.root_mem_glueCovered {squares component : Array Hex.DyadicSquare} {prec : ℤ} {z : ℂ} (hprec : ∀ u ∈ squares.toList, u.prec = prec) (hnear : ∀ u ∈ squares.toList, ‖z - DyadicSquare.center u‖ ≤ 65 / 32 * Dyadic.toReal u.radiusHi) (hcover : ∃ t ∈ squares.toList, z ∈ DyadicSquare.closedSquare t) (hc : component ∈ (Hex.glueCovered squares).toList) : z ∈ Component.region { squares := component, candidateK := 1 }

If every retained square is sharply near the same root and one survivor actually contains that root, maximal gluing puts the root in every output component.

theorem HexRootsMathlib.refineAll_carries_root {p : Hex.ZPoly} (rep : Hex.RefinedIsolation p) {work : Array Hex.Component} {prec : ℤ} (hdepth : ↑(Hex.separationDepth p) ≤ prec + 1) (hprec : Worklist.AtPrec work prec) (hwithin : Worklist.Within work (↑rep).square.doubled) (hcover : RefinedIsolation.root rep ∈ Worklist.region work) {c : Hex.Component} (hc : c ∈ (Hex.Component.refineAll p work).toList) : RefinedIsolation.root rep ∈ Component.region c

Every component of a sufficiently fine confined refinement round contains the represented simple root.

theorem HexRootsMathlib.refineAll_success {p : Hex.ZPoly} (rep : Hex.RefinedIsolation p) {work : Array Hex.Component} {prec target : ℤ} (hdepth : ↑(Hex.separationDepth p) + 5 ≤ prec + 1) (htarget : target + 5 ≤ prec + 1) (hprec : Worklist.AtPrec work prec) (hwithin : Worklist.Within work (↑rep).square.doubled) (hcover : RefinedIsolation.root rep ∈ Worklist.region work) : ∃ (c : Hex.Component) (iso : Hex.DyadicRootIsolation p), Hex.Component.refineAll p work = #[c] ∧ Hex.Component.certify? p Hex.AtomStrategy.nkThenPellet c = some (Hex.Certified.atom iso) ∧ target ≤ iso.square.prec

At the last normalized round, a confined one-atom worklist becomes one component and that component returns a target-ready mixed-strategy atom.

theorem HexRootsMathlib.refineLoop_complete {p : Hex.ZPoly} (rep : Hex.RefinedIsolation p) {target prec : ℤ} {work : Array Hex.Component} (hprec : Worklist.AtPrec work prec) (hwithin : Worklist.Within work (↑rep).square.doubled) (hcover : RefinedIsolation.root rep ∈ Worklist.region work) (hlt : prec < Hex.completenessDepth p target) {fuel : ℕ} (hfuel : (Hex.completenessDepth p target - prec).toNat < fuel) : ∃ (iso : Hex.DyadicRootIsolation p), Hex.refineLoop p target Hex.AtomStrategy.nkThenPellet fuel work = some #[Hex.Certified.atom iso]

Sufficient fuel carries a confined one-atom worklist through the globally reglued prefix and emits its unique target-ready mixed-strategy atom.

theorem HexRootsMathlib.DyadicRootIsolation.refineTo?_isSome_mixed {p : Hex.ZPoly} (rep : Hex.RefinedIsolation p) (target : ℤ) : ((↑rep).refineTo? target).isSome = true

Raw refinement of an already separation-refined atom is total for the mixed strategy. The bounded speculative pass may return first; otherwise the globally reglued NK-complete loop discharges the fallback. Pure Pellet completeness is deliberately not claimed here.

theorem HexRootsMathlib.RefinedIsolation.refineTo?_isSome_mixed {p : Hex.ZPoly} (rep : Hex.RefinedIsolation p) (target : ℤ) : (rep.refineTo? target).isSome = true

Refined-level refinement is total for the default mixed strategy.