Characteristic-Polynomial Saturation of Power Traces

Abstract

Cayley-Hamilton bounds the recurrence depth of every matrix power trace.

Theorem 1.1 (The first dimension-many traces determine all later traces).

$$\begin{array}{r}\forall K:\mathrm{Type},\mathrm{Field}\left(K\right),n\in \mathbb{N},\\ A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right)\Rightarrow \\ (A^n=-\sum _{k<n}\mathrm{coeff}\left(\mathrm{charpoly}\left(A\right),k\right)\times A^k)\wedge \\ (\forall m\in \mathbb{N},\mathrm{tr}\left(A^{n+m}\right)=-\sum _{k<n}\mathrm{coeff}\left(\mathrm{charpoly}\left(A\right),k\right)\times \mathrm{tr}\left(A^{k+m}\right))\wedge \\ \forall B\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right),(\mathrm{charpoly}\left(B\right)=\mathrm{charpoly}\left(A\right)\wedge \forall k\in \mathbb{N},k<n\Rightarrow \mathrm{tr}\left(A^{k+1}\right)=\mathrm{tr}\left(B^{k+1}\right))\Rightarrow \forall r\in \mathbb{N},\mathrm{tr}\left(A^{r+1}\right)=\mathrm{tr}\left(B^{r+1}\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

For an n-by-n matrix over any field, its monic characteristic polynomial and Cayley-Hamilton identity express the nth power as the negative coefficient-weighted sum of lower powers.

Multiplication by a further power and linearity of the matrix trace give the displayed recurrence at every offset. Strong induction then shows that two matrices with the same characteristic polynomial and the same first n positive-power traces have all positive-power traces equal.

The formal result strengthens the source context: characteristic zero is unnecessary for this Cayley-Hamilton consequence. Pinned Mathlib supplies the canonical Cayley-Hamilton theorem; repository and library searches found no exact result packaging all three public clauses.

References

• Truth anchor: D5/S0/Observation/PowerTraceCharacteristicPolynomialSaturation.power_trace_characteristic_polynomial_saturation