theorem HexRootsMathlib.pellet {p : Polynomial ℂ} {n k : ℕ} {r : ℝ} (hn : p.natDegree < n) (hk : k < n) (hr : 0 ≤ r) (hdom : ∑ i ∈ (Finset.range n).erase k, ‖p.coeff i‖ * r ^ i < ‖p.coeff k‖ * r ^ k) : rootsInDisc p 0 r = k

Pellet's theorem. If the k-th term strictly dominates all other terms on a circle, then the polynomial has exactly k roots in its open disc, counted with multiplicity.

theorem HexRootsMathlib.pellet_ne_zero {p : Polynomial ℂ} {n k : ℕ} {r : ℝ} (hn : p.natDegree < n) (hk : k < n) (hdom : ∑ i ∈ (Finset.range n).erase k, ‖p.coeff i‖ * r ^ i < ‖p.coeff k‖ * r ^ k) {z : ℂ} (hz : z ∈ Metric.sphere 0 r) : Polynomial.eval z p ≠ 0

Under Pellet dominance the polynomial has no zero on the boundary circle.

theorem HexRootsMathlib.pelletAt_size {cs : Array Hex.GaussDyadic} {k : ℕ} {rlo rhi : Dyadic} (h : Hex.pelletAt cs k rlo rhi = true) : k < cs.size

A successful executable Pellet check names an actual stored coefficient.

theorem HexRootsMathlib.pelletAt_bound {cs : Array Hex.GaussDyadic} {k : ℕ} {rlo rhi : Dyadic} (h : Hex.pelletAt cs k rlo rhi = true) : ∑ 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

A successful executable Pellet check exposes its strict real coefficient-dominance inequality.

theorem HexRootsMathlib.pelletAt_dominates {p : Hex.ZPoly} {c : Hex.GaussDyadic} {k : ℕ} {rlo rhi : Dyadic} {r : ℝ} (h : Hex.pelletAt (Hex.taylor p c) k rlo rhi = true) (hrlo : 0 ≤ Dyadic.toReal rlo) (hlo : Dyadic.toReal rlo ≤ r) (hhi : r ≤ Dyadic.toReal rhi) : have q := (toPolyℂ p).comp (Polynomial.X + Polynomial.C (GaussDyadic.toComplex c)); ∑ i ∈ (Finset.range (Hex.DensePoly.size p)).erase k, ‖q.coeff i‖ * r ^ i < ‖q.coeff k‖ * r ^ k

Dyadic lower and upper coefficient/radius bounds imply the exact coefficient dominance required by Pellet's theorem.

theorem HexRootsMathlib.pelletAt_rootsInDisc {p : Hex.ZPoly} {c : Hex.GaussDyadic} {k : ℕ} {rlo rhi : Dyadic} {r : ℝ} (h : Hex.pelletAt (Hex.taylor p c) k rlo rhi = true) (hrlo : 0 ≤ Dyadic.toReal rlo) (hlo : Dyadic.toReal rlo ≤ r) (hhi : r ≤ Dyadic.toReal rhi) : rootsInDisc ((toPolyℂ p).comp (Polynomial.X + Polynomial.C (GaussDyadic.toComplex c))) 0 r = k

One successful executable check implies exact Pellet soundness for any real radius lying between the supplied dyadic lower and upper bounds.

theorem HexRootsMathlib.pelletAt_ne_zero {p : Hex.ZPoly} {c : Hex.GaussDyadic} {k : ℕ} {rlo rhi : Dyadic} {r : ℝ} (h : Hex.pelletAt (Hex.taylor p c) k rlo rhi = true) (hrlo : 0 ≤ Dyadic.toReal rlo) (hlo : Dyadic.toReal rlo ≤ r) (hhi : r ≤ Dyadic.toReal rhi) {z : ℂ} (hz : z ∈ Metric.sphere 0 r) : Polynomial.eval z ((toPolyℂ p).comp (Polynomial.X + Polynomial.C (GaussDyadic.toComplex c))) ≠ 0

The same executable check excludes roots from the boundary circle at every real radius between its dyadic bounds.

theorem HexRootsMathlib.rootsInDisc_comp_X_add_C (p : Polynomial ℂ) (c : ℂ) (r : ℝ) : rootsInDisc (p.comp (Polynomial.X + Polynomial.C c)) 0 r = rootsInDisc p c r

Translating the variable translates every root without changing its multiplicity or its membership in the corresponding open disc.

theorem HexRootsMathlib.rootsInDisc_localPoly (p : Hex.ZPoly) (s : Hex.DyadicSquare) (r : ℝ) : rootsInDisc (localPoly p s) 0 r = rootsInDisc (toPolyℂ p) (DyadicSquare.center s) (Dyadic.toReal (Dyadic.ofIntWithPrec 1 s.prec) * r)

Scaling to square-local coordinates scales the counted disc radius by the square half-width.

theorem HexRootsMathlib.pelletAt_ne_zero_center {p : Hex.ZPoly} {c : Hex.GaussDyadic} {k : ℕ} {rlo rhi : Dyadic} {r : ℝ} (h : Hex.pelletAt (Hex.taylor p c) k rlo rhi = true) (hrlo : 0 ≤ Dyadic.toReal rlo) (hlo : Dyadic.toReal rlo ≤ r) (hhi : r ≤ Dyadic.toReal rhi) {z : ℂ} (hz : z ∈ Metric.sphere (GaussDyadic.toComplex c) r) : Polynomial.eval z (toPolyℂ p) ≠ 0

The executable check excludes roots from the corresponding circle about the original Taylor centre.

theorem HexRootsMathlib.PelletWitness.witness_cases {p : Hex.ZPoly} {s : Hex.DyadicSquare} {k : ℕ} (h : Hex.witness p s k) : Hex.softWitnessCheck p s k = true ∨ Hex.TaylorShift.witnessCheck s (Hex.TaylorShift.compute p s.center) k = true

The public witness is either the bounded-precision Graeffe path or the exact Taylor fallback.

theorem HexRootsMathlib.PelletWitness.soft_roots {p : Hex.ZPoly} {s : Hex.DyadicSquare} {k : ℕ} (h : Hex.softWitnessCheck p s k = true) : rootsInDisc (toPolyℂ p) (DyadicSquare.center s) (DyadicSquare.radius s) = k

A successful soft Graeffe check certifies the base circumscribed disc.

theorem HexRootsMathlib.PelletWitness.soft_roots_two {p : Hex.ZPoly} {s : Hex.DyadicSquare} {k : ℕ} (h : Hex.softWitnessCheck p s k = true) : rootsInDisc (toPolyℂ p) (DyadicSquare.center s) (2 * DyadicSquare.radius s) = k

A successful soft Graeffe check certifies the doubled disc.

theorem HexRootsMathlib.PelletWitness.soft_roots_four {p : Hex.ZPoly} {s : Hex.DyadicSquare} {k : ℕ} (h : Hex.softWitnessCheck p s k = true) : rootsInDisc (toPolyℂ p) (DyadicSquare.center s) (4 * DyadicSquare.radius s) = k

A successful soft Graeffe check certifies the quadrupled disc.

theorem HexRootsMathlib.PelletWitness.checks {p : Hex.ZPoly} {s : Hex.DyadicSquare} {k : ℕ} (h : Hex.TaylorShift.witnessCheck s (Hex.TaylorShift.compute p s.center) k = true) : (Hex.pelletAt (Hex.taylor p s.center) k s.radiusLo s.radiusHi = true ∧ Hex.pelletAt (Hex.taylor p s.center) k (s.radiusLo <<< 1) (s.radiusHi <<< 1) = true) ∧ Hex.pelletAt (Hex.taylor p s.center) k (s.radiusLo <<< 2) (s.radiusHi <<< 2) = true

The three Boolean checks contained in an executable witness.

theorem HexRootsMathlib.PelletWitness.roots {p : Hex.ZPoly} {s : Hex.DyadicSquare} {k : ℕ} (h : Hex.witness p s k) : rootsInDisc (toPolyℂ p) (DyadicSquare.center s) (DyadicSquare.radius s) = k

A Pellet witness certifies exactly k roots in the square's circumscribed open disc.

theorem HexRootsMathlib.PelletWitness.roots_two {p : Hex.ZPoly} {s : Hex.DyadicSquare} {k : ℕ} (h : Hex.witness p s k) : rootsInDisc (toPolyℂ p) (DyadicSquare.center s) (2 * DyadicSquare.radius s) = k

The second check certifies the same root count in the doubled disc.

theorem HexRootsMathlib.PelletWitness.roots_four {p : Hex.ZPoly} {s : Hex.DyadicSquare} {k : ℕ} (h : Hex.witness p s k) : rootsInDisc (toPolyℂ p) (DyadicSquare.center s) (4 * DyadicSquare.radius s) = k

The third check certifies the same root count in the quadrupled disc.

theorem HexRootsMathlib.PelletWitness.boundary {p : Hex.ZPoly} {s : Hex.DyadicSquare} {k : ℕ} (h : Hex.witness p s k) {z : ℂ} (hz : z ∈ Metric.sphere (DyadicSquare.center s) (DyadicSquare.radius s)) : Polynomial.eval z (toPolyℂ p) ≠ 0

The strict base-radius inequality excludes boundary roots.

theorem HexRootsMathlib.PelletWitness.boundary_two {p : Hex.ZPoly} {s : Hex.DyadicSquare} {k : ℕ} (h : Hex.witness p s k) {z : ℂ} (hz : z ∈ Metric.sphere (DyadicSquare.center s) (2 * DyadicSquare.radius s)) : Polynomial.eval z (toPolyℂ p) ≠ 0

The doubled-radius inequality excludes boundary roots.

theorem HexRootsMathlib.PelletWitness.boundary_four {p : Hex.ZPoly} {s : Hex.DyadicSquare} {k : ℕ} (h : Hex.witness p s k) {z : ℂ} (hz : z ∈ Metric.sphere (DyadicSquare.center s) (4 * DyadicSquare.radius s)) : Polynomial.eval z (toPolyℂ p) ≠ 0

The quadrupled-radius inequality excludes boundary roots.

theorem HexRootsMathlib.PelletWitness.sound {p : Hex.ZPoly} {s : Hex.DyadicSquare} (h : Hex.witness p s 1) : ∃ (z : ℂ), Polynomial.eval z (toPolyℂ p) = 0 ∧ z ∈ DyadicSquare.disc s ∧ Polynomial.eval z (Polynomial.derivative (toPolyℂ p)) ≠ 0 ∧ ∀ (w : ℂ), Polynomial.eval w (toPolyℂ p) = 0 → w ∈ DyadicSquare.closedDisc s → w = z

The k = 1 Pellet disjunct certifies one interior simple root, unique in the closed circumscribed disc.

theorem HexRootsMathlib.DyadicRootCluster.roots {p : Hex.ZPoly} (cl : Hex.DyadicRootCluster p) : rootsInDisc (toPolyℂ p) (DyadicSquare.center (Hex.encSquare cl.squares)) (DyadicSquare.radius (Hex.encSquare cl.squares)) = cl.k

A certified cluster contains exactly its stored multiplicity count in the enclosing square's circumscribed disc.

theorem HexRootsMathlib.DyadicRootCluster.boundary {p : Hex.ZPoly} (cl : Hex.DyadicRootCluster p) {z : ℂ} (hz : z ∈ Metric.sphere (DyadicSquare.center (Hex.encSquare cl.squares)) (DyadicSquare.radius (Hex.encSquare cl.squares))) : Polynomial.eval z (toPolyℂ p) ≠ 0

A certified cluster has no root on the boundary of its certified disc.