theorem HexRootsMathlib.choose_eq_choose (n k : ℕ) : Hex.Nat.choose n k = n.choose k

The Mathlib and Mathlib-free Pascal recursions define the same binomial coefficient.

theorem HexRootsMathlib.toComplex_gaussSum (n : ℕ) (f : ℕ → Hex.GaussDyadic) : GaussDyadic.toComplex (Hex.gaussSum n f) = ∑ i ∈ Finset.range n, GaussDyadic.toComplex (f i)

Casting the executable finite Gaussian-dyadic sum gives a Finset sum in ℂ.

theorem HexRootsMathlib.toComplex_taylorCoeff (p : Hex.ZPoly) (z : Hex.GaussDyadic) (k : ℕ) : GaussDyadic.toComplex (Hex.taylorCoeff p z k) = ∑ r ∈ Finset.range (Hex.DensePoly.size p - k), ↑((k + r).choose k) * ↑(Hex.DensePoly.coeff p (k + r)) * GaussDyadic.toComplex z ^ r

The executable closed-form Taylor coefficient casts to its ordinary complex binomial sum.

theorem HexRootsMathlib.coeff_shift (p : Hex.ZPoly) (z : Hex.GaussDyadic) (k : ℕ) : ((toPolyℂ p).comp (Polynomial.X + Polynomial.C (GaussDyadic.toComplex z))).coeff k = ∑ r ∈ Finset.range (Hex.DensePoly.size p - k), ↑((k + r).choose k) * ↑(Hex.DensePoly.coeff p (k + r)) * GaussDyadic.toComplex z ^ r

Coefficient k of the Mathlib Taylor shift is the same finite binomial sum used by the executable implementation.

theorem HexRootsMathlib.taylor_coeff (p : Hex.ZPoly) (z : Hex.GaussDyadic) (k : ℕ) : GaussDyadic.toComplex ((Hex.taylor p z).getD k (0, 0)) = ((toPolyℂ p).comp (Polynomial.X + Polynomial.C (GaussDyadic.toComplex z))).coeff k

Taylor bridge. Every executable Taylor array entry, including an out-of-bounds getD, casts to the corresponding coefficient of the exact Mathlib shift p(X + z).