theorem HexRootsMathlib.DyadicSquare.closedSquare_subset_of_mem_subdivide {s t : Hex.DyadicSquare} (ht : t ∈ s.subdivide.toList) : closedSquare t ⊆ closedSquare s

Every closed child square returned by subdivision is contained in its parent closed square.

theorem HexRootsMathlib.DyadicSquare.exists_mem_subdivide {s : Hex.DyadicSquare} {z : ℂ} (hz : z ∈ closedSquare s) : ∃ t ∈ s.subdivide.toList, z ∈ closedSquare t

The four closed children returned by executable subdivision cover their parent square.

theorem HexRootsMathlib.exists_mem_subdivideAll {squares : Array Hex.DyadicSquare} {z : ℂ} {s : Hex.DyadicSquare} (hs : s ∈ squares.toList) (hz : z ∈ DyadicSquare.closedSquare s) : ∃ t ∈ (Array.flatMap Hex.DyadicSquare.subdivide squares).toList, z ∈ DyadicSquare.closedSquare t

Subdividing every square in an array preserves coverage of their union.

theorem HexRootsMathlib.isRoot_mem_survivors {p : Hex.ZPoly} {squares : Array Hex.DyadicSquare} {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) {s : Hex.DyadicSquare} (hs : s ∈ squares.toList) (hz : z ∈ DyadicSquare.closedSquare s) : ∃ t ∈ (Array.filter (fun (u : Hex.DyadicSquare) => !Hex.rootFree p u) (Array.flatMap Hex.DyadicSquare.subdivide squares)).toList, z ∈ DyadicSquare.closedSquare t

A child containing a root survives the elementary T₀ filter.