Newton's Identities for Matrices

Newton's identities (Faddeev–LeVerrier recurrence) relate the traces of powers of a matrix to the coefficients of its characteristic polynomial.

Main results

• Matrix.newton_trace_charpoly — the Newton identity at step k: tr(A^k) + ∑_{j=1}^{k-1} c_{|n|-j} · tr(A^{k-j}) + k · c_{|n|-k} = 0

• Matrix.cayley_hamilton_trace — the Cayley–Hamilton trace identity: ∑_{i=0}^{n} c_i · tr(A^i) = 0, which is Newton at k = n

Proof strategy

The proof of Newton's identity combines two ingredients:

1. Trace of adjugate = derivative. The trace of adjugate(charmatrix A) equals derivative(charpoly A). This follows from the fact that diagonal entries of the adjugate are principal subdeterminants, which sum to the derivative by the Jacobi/Leibniz formula (derivative_det_charmatrix from Spectral.lean).

2. Adjugate coefficient recurrence. From mul_adjugate, the polynomial-coefficient matrices of adjugate(charmatrix A) satisfy a Faddeev–LeVerrier recurrence: B_{m-1} = A * B_m + c_m • I, with B_{N-1} = I. By induction: B_{N-1-k} = A^k + c_{N-1} A^{k-1} + ⋯ + c_{N-k} I.

Combining: the coefficient of x^{N-1-k} in derivative(charpoly) is (N-k) c_{N-k}, and the trace of B_{N-1-k} is s_k + ∑ c_{N-j} s_{k-j} + N c_{N-k}. Equating gives Newton's identity.

References

• Faddeev, D. K. & Faddeeva, V. N. (1963). Computational Methods of Linear Algebra.
• Newton, I. (1707). Arithmetica Universalis.

Adjugate diagonal = principal subdeterminant

Trace of adjugate of charmatrix = characteristic polynomial derivative

Coefficient extraction from mul_adjugate

Adjugate coefficient formula by induction

Cayley–Hamilton trace identity

theorem Matrix.cayley_hamilton_trace {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (A : Matrix n n R) : ∑ i ∈ Finset.range (Fintype.card n + 1), A.charpoly.coeff i * (A ^ i).trace = 0

Cayley–Hamilton trace identity. Taking the trace of p(A) = 0 (Cayley–Hamilton) yields:

∑_{i=0}^{n} charpoly.coeff(i) · tr(A^i) = 0

Newton's identity

theorem Matrix.newton_trace_charpoly {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (A : Matrix n n R) {k : ℕ} (hk : 1 ≤ k) (hk' : k ≤ Fintype.card n) : (A ^ k).trace + ∑ j ∈ Finset.range (k - 1), A.charpoly.coeff (Fintype.card n - (j + 1)) * (A ^ (k - (j + 1))).trace + ↑k * A.charpoly.coeff (Fintype.card n - k) = 0

Newton's identity at step k. For a matrix A over a commutative ring and 1 ≤ k ≤ |n|:

tr(A^k) + ∑_{j=1}^{k-1} c_{|n|-j} · tr(A^{k-j}) + k · c_{|n|-k} = 0

where c_i denotes A.charpoly.coeff i.