Newton Power Sums Determine the Characteristic Polynomial

Abstract

Newton identities recover a split characteristic polynomial from its bounded power sums.

Theorem 1.1 (The first dimension-many spectral power sums determine the charpoly).

$$\begin{array}{r}\forall K:\mathrm{Type},\mathrm{Field}\left(K\right),\mathrm{CharZero}\left(K\right),n\in \mathbb{N},\\ \forall A,B\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right),lambda,mu\in \mathrm{Fin}\left(n\right)\to K,\\ (\mathrm{charpoly}\left(A\right)=\prod _{i\in \mathrm{Fin}\left(n\right)}(t-lambda(i))\wedge \mathrm{charpoly}\left(B\right)=\prod _{i\in \mathrm{Fin}\left(n\right)}(t-mu(i))\wedge \forall k\in \mathbb{N},k<n\Rightarrow \sum _{i\in \mathrm{Fin}\left(n\right)}lambda(i{)}^{k+1}=\sum _{i\in \mathrm{Fin}\left(n\right)}mu(i{)}^{k+1})\Rightarrow \\ \mathrm{charpoly}\left(A\right)=\mathrm{charpoly}\left(B\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S0/Observation/NewtonPowerSumCharacteristicPolynomial.matrix_charpoly_eq_of_spectral_power_sums_eq (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let two n-by-n matrices over a characteristic-zero field have enumerated split spectra. If the first n positive power sums of those spectra agree, then their characteristic polynomials agree.

Pinned Mathlib’s Newton identity recursively recovers each elementary symmetric polynomial because every positive natural number is nonzero in the field. Mathlib’s Vieta expansion then identifies the two products of linear factors.

Characteristic zero is explicit: without it, the natural-number factor in the Newton recurrence cannot always be cancelled. The split factorization hypotheses expose the spectral witnesses used by the source argument rather than assuming an unavailable trace-to-root bridge.

References

• Truth anchor: D5/S0/Observation/NewtonPowerSumCharacteristicPolynomial.matrix_charpoly_eq_of_spectral_power_sums_eq