theorem HexRootsMathlib.pelletAt_zero_of_slack {p : Hex.ZPoly} {c : Hex.GaussDyadic} {rlo rhi : Dyadic} (hsize : 0 < Hex.DensePoly.size p) (hrhi : 0 ≤ Dyadic.toReal rhi) (hslack : 2 * ∑ i ∈ (Finset.range (Hex.DensePoly.size p)).erase 0, ‖((toPolyℂ p).comp (Polynomial.X + Polynomial.C (GaussDyadic.toComplex c))).coeff i‖ * Dyadic.toReal rhi ^ i < ‖((toPolyℂ p).comp (Polynomial.X + Polynomial.C (GaussDyadic.toComplex c))).coeff 0‖) : Hex.pelletAt (Hex.taylor p c) 0 rlo rhi = true

A factor-two exact-norm margin at coefficient zero absorbs both Gaussian dyadic coefficient bounds and makes the executable Pellet check succeed.

theorem HexRootsMathlib.rootFree_one_root_of_margin {p : Hex.ZPoly} {sq : Hex.DyadicSquare} {z : ℂ} {roots : Multiset ℂ} {d : ℝ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hroots : (toPolyℂ p).roots = z ::ₘ roots) (hd : 0 < d) (hremote : ∀ w ∈ roots, d ≤ ‖w - DyadicSquare.center sq‖) (hmargin : have R := Dyadic.toReal sq.radiusHi; have E := (1 + R / d) ^ roots.card - 1; 2 * (R + (R + ‖z - DyadicSquare.center sq‖) * E) < ‖z - DyadicSquare.center sq‖) : Hex.rootFree p sq = true

If one root is separated from all the others and is far enough from the centre relative to the test radius, the actual executable T-zero test succeeds. The contrapositive gives the constant-radius survivor bound used by the glue argument.

theorem HexRootsMathlib.rootFree_of_roots {p : Hex.ZPoly} {s : Hex.DyadicSquare} {d : ℝ} (hp : toPolyℂ p ≠ 0) (hsize : 0 < Hex.DensePoly.size p) (hd : 0 < d) (hremote : ∀ z ∈ (toPolyℂ p).roots, d ≤ ‖z - DyadicSquare.center s‖) (htail : 2 * ((1 + Dyadic.toReal s.radiusHi / d) ^ (toPolyℂ p).roots.card - 1) < 1) : Hex.rootFree p s = true

If every root is remote enough that the normalized positive-degree tail has mass below one half, the actual executable rootFree test succeeds.

theorem HexRootsMathlib.exists_root_ne_of_not_rootFree {p : Hex.ZPoly} {s : Hex.DyadicSquare} (hp : toPolyℂ p ≠ 0) (hsize : 0 < Hex.DensePoly.size p) (hkeep : Hex.rootFree p s ≠ true) : ∃ z ∈ (toPolyℂ p).roots, ‖z - DyadicSquare.center s‖ < 8 * ↑(Nat.max 2 (Hex.DensePoly.natDegree p)) * Dyadic.toReal s.radiusHi

A square retained by the T-zero filter lies within eight degree-scaled upper radii of an actual root.

theorem HexRootsMathlib.exists_root_ne_of_depth {p : Hex.ZPoly} {s : Hex.DyadicSquare} (hp : toPolyℂ p ≠ 0) (hsize : 0 < Hex.DensePoly.size p) (hprec : ↑(Hex.separationDepth p) ≤ s.prec) (hkeep : Hex.rootFree p s ≠ true) : ∃ z ∈ (toPolyℂ p).roots, ‖z - DyadicSquare.center s‖ < 2 ^ (-↑(Hex.mahlerPrec p)) * (1449 / 1024) / 32

At separationDepth, every retained square is extremely close to one root on the Mahler separation scale.

theorem HexRootsMathlib.root_near_of_simple {p : Hex.ZPoly} {s : Hex.DyadicSquare} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hsimple : Polynomial.eval z (Polynomial.derivative (toPolyℂ p)) ≠ 0) (hprec : ↑(Hex.separationDepth p) ≤ s.prec) (hkeep : Hex.rootFree p s ≠ true) (hzc : ‖z - DyadicSquare.center s‖ < 2 ^ (-↑(Hex.mahlerPrec p)) * (1449 / 1024) / 32) : ‖z - DyadicSquare.center s‖ ≤ 65 / 32 * Dyadic.toReal s.radiusHi

Once a locally simple root has been identified on the coarse Mahler scale, failure of T₀ places it within the sharp degree-independent survivor radius. Other roots of the polynomial may have multiplicity.

theorem HexRootsMathlib.exists_root_le_radius_of_not_rootFree {p : Hex.ZPoly} {s : Hex.DyadicSquare} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hprec : ↑(Hex.separationDepth p) ≤ s.prec) (hkeep : Hex.rootFree p s ≠ true) : ∃ z ∈ (toPolyℂ p).roots, ‖z - DyadicSquare.center s‖ ≤ 65 / 32 * Dyadic.toReal s.radiusHi

At separation depth the remote-root tail is already negligible, so a square retained by T-zero is within 65/32 executable radii of one root. The 1/384 tail at the implemented depth leaves enough room for enclosing a whole component with a loss of at most two precision levels.

theorem HexRootsMathlib.DyadicSquare.supDist_center_lt_of_adjacent {s t : Hex.DyadicSquare} (hadj : s.adjacent t = true) : s.prec = t.prec ∧ supDist (center s) (center t) < 4 * halfWidth s

Executable edge-or-corner adjacency is strictly less than four half-widths in the sup metric.

theorem HexRootsMathlib.DyadicSquare.adjacent_of_supDist_lt {s t : Hex.DyadicSquare} (hprec : s.prec = t.prec) (hdist : supDist (center s) (center t) < 4 * halfWidth s) : s.adjacent t = true

The geometric same-precision bound is also sufficient for executable adjacency.

theorem HexRootsMathlib.exists_common_nearRoot_of_adjacent {p : Hex.ZPoly} {s t : Hex.DyadicSquare} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hprec : ↑(Hex.separationDepth p) ≤ s.prec) (hs : Hex.rootFree p s ≠ true) (ht : Hex.rootFree p t ≠ true) (hadj : s.adjacent t = true) : ∃ z ∈ (toPolyℂ p).roots, ‖z - DyadicSquare.center s‖ ≤ 65 / 32 * Dyadic.toReal s.radiusHi ∧ ‖z - DyadicSquare.center t‖ ≤ 65 / 32 * Dyadic.toReal t.radiusHi

Adjacent retained squares at separation depth have the same nearby root, with the sharp degree-independent bound on both centres.

def HexRootsMathlib.NearRoot (p : Hex.ZPoly) (s : Hex.DyadicSquare) (z : ℂ) : Prop

A root is in the degree-independent proximity neighborhood of a retained square.

Equations

• HexRootsMathlib.NearRoot p s z = (z ∈ (HexRootsMathlib.toPolyℂ p).roots ∧ ‖z - HexRootsMathlib.DyadicSquare.center s‖ ≤ 65 / 32 * HexRootsMathlib.Dyadic.toReal s.radiusHi)

theorem HexRootsMathlib.nearRoot_unique {p : Hex.ZPoly} {s : Hex.DyadicSquare} (hp : toPolyℂ p ≠ 0) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hprec : ↑(Hex.separationDepth p) ≤ s.prec) {z w : ℂ} (hz : NearRoot p s z) (hw : NearRoot p s w) : z = w

Mahler separation makes the nearby root of a separation-depth square unique.

theorem HexRootsMathlib.nearRoot_iff_of_edge {p : Hex.ZPoly} {s t : Hex.DyadicSquare} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hprec : ∀ (u : Hex.DyadicSquare), u = s ∨ u = t → ↑(Hex.separationDepth p) ≤ u.prec) (hkeep : ∀ (u : Hex.DyadicSquare), u = s ∨ u = t → Hex.rootFree p u ≠ true) (hedge : Glue.Edge s t) (z : ℂ) : NearRoot p s z ↔ NearRoot p t z

Crossing one retained adjacency edge preserves the semantic nearby root.

theorem HexRootsMathlib.nearRoot_iff_of_connected {p : Hex.ZPoly} {component : List Hex.DyadicSquare} {s t : Hex.DyadicSquare} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hconnected : Glue.Connected component) (hprec : ∀ u ∈ component, ↑(Hex.separationDepth p) ≤ u.prec) (hkeep : ∀ u ∈ component, Hex.rootFree p u ≠ true) (hs : s ∈ component) (ht : t ∈ component) (z : ℂ) : NearRoot p s z ↔ NearRoot p t z

Nearby-root semantics is constant on a connected retained component.

theorem HexRootsMathlib.exists_nearRoot_of_connected {p : Hex.ZPoly} {component : List Hex.DyadicSquare} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hconnected : Glue.Connected component) (hprec : ∀ u ∈ component, ↑(Hex.separationDepth p) ≤ u.prec) (hkeep : ∀ u ∈ component, Hex.rootFree p u ≠ true) : ∃ z ∈ (toPolyℂ p).roots, ∀ u ∈ component, ‖z - DyadicSquare.center u‖ ≤ 65 / 32 * Dyadic.toReal u.radiusHi

Every connected component of retained separation-depth squares has one root satisfying the sharp proximity bound at every member.

theorem HexRootsMathlib.exists_nearRoot_of_glueCovered {p : Hex.ZPoly} {squares component : Array Hex.DyadicSquare} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hprec : ∀ u ∈ squares.toList, ↑(Hex.separationDepth p) ≤ u.prec) (hkeep : ∀ u ∈ squares.toList, Hex.rootFree p u ≠ true) (hc : component ∈ (Hex.glueCovered squares).toList) : ∃ z ∈ (toPolyℂ p).roots, ∀ u ∈ component.toList, ‖z - DyadicSquare.center u‖ ≤ 65 / 32 * Dyadic.toReal u.radiusHi

Every actual glued component of retained separation-depth squares belongs to one root, uniformly satisfying the sharp proximity bound.