theorem HexRootsMathlib.pelletFold (cs : Array Hex.GaussDyadic) (k : ℕ) (r : Dyadic) (n : ℕ) : have result := List.foldl (fun (acc : Dyadic × Dyadic) (i : ℕ) => have acc' := if i = k then acc.1 else acc.1 + (cs.getD i (0, 0)).hi * acc.2; (acc', acc.2 * r)) (0, 1) (List.range n); (Dyadic.toReal result.1 = ∑ i ∈ Finset.range n, if i = k then 0 else Dyadic.toReal (cs.getD i (0, 0)).hi * Dyadic.toReal r ^ i) ∧ Dyadic.toReal result.2 = Dyadic.toReal r ^ n

Closed form of the accumulator used by pelletAt: its first component is the sum with coefficient k omitted, and its second component is the next power of the radius. Shared by the elementary rootFree proof here and the general Pellet correspondence in Pellet.lean.

theorem HexRootsMathlib.exactRootFree_size_pos {p : Hex.ZPoly} {s : Hex.DyadicSquare} (h : Hex.exactRootFree p s = true) : 0 < Hex.DensePoly.size p

A successful root-exclusion test can only occur for a nonempty stored polynomial.

theorem HexRootsMathlib.shift_natDegree_lt_size (p : Hex.ZPoly) (hp : 0 < Hex.DensePoly.size p) (c : ℂ) : ((toPolyℂ p).comp (Polynomial.X + Polynomial.C c)).natDegree < Hex.DensePoly.size p

A nonempty polynomial's shift has degree strictly below its executable coefficient count. Shared by the elementary and general Pellet proofs.

theorem HexRootsMathlib.exactRootFree_bound {p : Hex.ZPoly} {s : Hex.DyadicSquare} (h : Hex.exactRootFree p s = true) : (∑ i ∈ Finset.range (Hex.DensePoly.size p), if i = 0 then 0 else Dyadic.toReal ((Hex.taylor p s.center).getD i (0, 0)).hi * Dyadic.toReal s.radiusHi ^ i) < Dyadic.toReal ((Hex.taylor p s.center).getD 0 (0, 0)).lo

The Boolean rootFree result exposes the strict real Taylor-dominance inequality used by its soundness proof.

theorem HexRootsMathlib.rootFree_ne_zero {p : Hex.ZPoly} {s : Hex.DyadicSquare} (h : Hex.rootFree p s = true) {z : ℂ} (hz : z ∈ Metric.ball (DyadicSquare.center s) (Dyadic.toReal s.radiusHi)) : Polynomial.eval z (toPolyℂ p) ≠ 0

Combined T₀ soundness. The bounded-precision filter and the exact Taylor fallback both exclude every zero from the executable upper-radius disc.

theorem HexRootsMathlib.rootFree_closedSquare {p : Hex.ZPoly} {s : Hex.DyadicSquare} (h : Hex.rootFree p s = true) {z : ℂ} (hz : z ∈ DyadicSquare.closedSquare s) : Polynomial.eval z (toPolyℂ p) ≠ 0

A successful rootFree test excludes roots from the represented closed square.

theorem HexRootsMathlib.rootFree_closedDisc {p : Hex.ZPoly} {s : Hex.DyadicSquare} (h : Hex.rootFree p s = true) {z : ℂ} (hz : z ∈ DyadicSquare.closedDisc s) : Polynomial.eval z (toPolyℂ p) ≠ 0

The stated circumscribed closed disc is root-free as well; its radius is strictly below the executable upper-radius bound used by rootFree.