theorem HexRootsMathlib.pelletAt_of_bound {cs : Array Hex.GaussDyadic} {k : ℕ} {rlo rhi : Dyadic} (hk : k < cs.size) (hbound : ∑ i ∈ (Finset.range cs.size).erase k, Dyadic.toReal (cs.getD i (0, 0)).hi * Dyadic.toReal rhi ^ i < Dyadic.toReal (cs.getD k (0, 0)).lo * Dyadic.toReal rlo ^ k) : Hex.pelletAt cs k rlo rhi = true

Converse to pelletAt_bound: a strict inequality between the exact real casts of the dyadic bounds makes the executable Boolean check succeed.

theorem HexRootsMathlib.pelletAt_one_of_slack {p : Hex.ZPoly} {c : Hex.GaussDyadic} {rlo rhi : Dyadic} (hsize : 1 < Hex.DensePoly.size p) (hrlo : 0 ≤ Dyadic.toReal rlo) (hrhi : 0 ≤ Dyadic.toReal rhi) (hslack : 2 * ∑ i ∈ (Finset.range (Hex.DensePoly.size p)).erase 1, ‖((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 1‖ * Dyadic.toReal rlo) : Hex.pelletAt (Hex.taylor p c) 1 rlo rhi = true

A factor-two exact-norm margin absorbs both Gaussian-dyadic coefficient bounds. The two radii may differ, matching the executable lower radius on the dominant term and upper radius on the omitted tail.

theorem HexRootsMathlib.pellet_one_comp_slack {p : Polynomial ℂ} {c z : ℂ} {s : Multiset ℂ} {d R r L : ℝ} (hp : p ≠ 0) (hroots : p.roots = z ::ₘ s) (hd : 0 < d) (hR : 0 ≤ R) (hr : 0 ≤ r) (hrR : r ≤ R) (hL : 0 ≤ L) (hremote : ∀ w ∈ s, d ≤ ‖w - c‖) (hmargin : L * ‖z - c‖ + (L * R + (2 * L + 1) * ‖z - c‖) * ((1 + R / d) ^ s.card - 1) < r) : L * ∑ i ∈ (Finset.range (s.card + 2)).erase 1, ‖(p.comp (Polynomial.X + Polynomial.C c)).coeff i‖ * R ^ i < ‖(p.comp (Polynomial.X + Polynomial.C c)).coeff 1‖ * r

Strengthened translation form of the exact Pellet converse. The multiplier and the two radii make the coefficient slack required by an executable enclosure explicit; pelletAt_one_of_slack consumes the case L = 2.

theorem HexRootsMathlib.exactWitness_one_of_roots {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 - GaussDyadic.toComplex sq.center‖) (hmargin : ∀ j < 3, have rlo := Dyadic.toReal (sq.radiusLo <<< ↑j); have rhi := Dyadic.toReal (sq.radiusHi <<< ↑j); 2 * ‖z - GaussDyadic.toComplex sq.center‖ + (2 * rhi + 5 * ‖z - GaussDyadic.toComplex sq.center‖) * ((1 + rhi / d) ^ roots.card - 1) < rlo) : Hex.TaylorShift.witnessCheck sq (Hex.TaylorShift.compute p sq.center) 1 = true

A wide one-root isolation satisfying the explicit enclosure margin at the base, doubled, and quadrupled radii makes the exact Taylor Pellet witness succeed. The remote multiset retains root multiplicity.

theorem HexRootsMathlib.witness_one_of_roots {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 - GaussDyadic.toComplex sq.center‖) (hmargin : ∀ j < 3, have rlo := Dyadic.toReal (sq.radiusLo <<< ↑j); have rhi := Dyadic.toReal (sq.radiusHi <<< ↑j); 2 * ‖z - GaussDyadic.toComplex sq.center‖ + (2 * rhi + 5 * ‖z - GaussDyadic.toComplex sq.center‖) * ((1 + rhi / d) ^ roots.card - 1) < rlo) : Hex.witness p sq 1

The exact completeness witness is accepted by the public soft-or-exact Pellet predicate.