Newton–Hankel Real-Root Criterion
Abstract
Negative real roots of a positive-coefficient polynomial are equivalent to positivity of its Newton–Hankel matrix.
Theorem 1.1 (Explicit evaluation interface for real interpolation).
Lean statement: D5/S3/Constants/NewtonHankelRealRootCriterion.exists_real_pair_interpolant
Proof. Machine-checked in Lean as D5/S3/Constants/NewtonHankelRealRootCriterion.exists_real_pair_interpolant (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every natural d, complex root vector on Fin d, and complex z in its finite image with conjugate(z) unequal to z, assume that membership in this finite image is invariant under complex conjugation. There exists a real coefficient vector on Fin d whose vectorPolynomialValue at every w in that image is i when w=z, minus i when w=conjugate(z), and zero otherwise. The original private interpolation construction is reused unchanged. This explicit interface is consumed by complete countable-spectrum head isolation; it is an organizational helper, not a second interpolation proof.
Theorem 1.2 (Positive coefficients give positive evaluation).
Proof. Machine-checked in Lean as D5/S3/Constants/NewtonHankelRealRootCriterion.eval_pos_of_positive_coefficients (✓ std3). ∎
Source. Repository-derived.
Commentary.
A real polynomial of degree d with strictly positive coefficients from zero through d has a strictly positive value at every nonnegative real argument. The displayed degree equality and coefficient inequalities are the definition of HasPositiveCoefficientsOfDegree. Every term in its evaluation sum is nonnegative, and its constant term is strictly positive.
Theorem 1.3 (Negative roots are equivalent to Newton–Hankel positivity).
Proof. Machine-checked in Lean as D5/S3/Constants/NewtonHankelRealRootCriterion.negative_real_roots_iff_newtonHankel_posSemidef (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let P be a real polynomial of degree d whose coefficients from degree zero through d are strictly positive. Let lambda enumerate with multiplicity the nonzero roots of q(x)=x^d P(-1/x), and assume its finite support is closed under complex conjugation. Then every root of P is a negative real number if and only if the normalized Newton–Hankel matrix G_d built from the lambda power sums is positive semidefinite.
The forward direction expands every quadratic form as the normalized sum of squares at real roots. For the reverse direction, a nonreal root and its conjugate are assigned interpolation values i and -i, with zero at every other distinct root. Lagrange interpolation descends to real coefficients and makes the quadratic form strictly negative. Positive coefficients then exclude nonpositive real roots of q, and the reversed-root correspondence gives the negative roots of P.
This declaration carries only properties one and two of the source theorem. It does not assert a positive-definite determinant realization or a nonnegative-weight Fibonacci-chain realization.