Trace Cayley-Hamilton / Newton identity

trace_cayley_hamilton_newton — a formalization challenge from the lean-eval benchmark.

Notes

The Newton trace recurrence for the coefficients of the characteristic polynomial: k cₖ + ∑{j=1}^k tr(Aʲ) c{k-j} = 0, where χ_A(X) = Xᴺ + c₁ Xᴺ⁻¹ + ⋯ + c_N. The helper charpolyDescendingCoeff packages cₖ as the degree N−k coefficient of Matrix.charpoly (zero for k > N), so the recurrence holds uniformly for all positive k. Mathlib has Cayley-Hamilton (Matrix.aeval_self_charpoly) but not the Newton trace identity relating power sums tr(Aʲ) to the elementary-symmetric charpoly coefficients. Category-(b) candidate.

Formal statement

/-- The trace Cayley-Hamilton / Newton identity:
`k c_k + ∑_{j=1}^k tr(A^j) c_{k-j} = 0`, where
`χ_A(X) = X^N + c₁ X^(N-1) + ... + c_N`.

For `k > N`, `c_k = 0`, and the remaining relation is the trace of
Cayley-Hamilton multiplied by a power of `A`. -/
theorem trace_cayley_hamilton_newton {R : Type*} [CommRing R]
    (A : Matrix n n R) {k : ℕ} (hk : 1 ≤ k) :
    (k : R) * charpolyDescendingCoeff A k +
        ∑ j ∈ Finset.Icc 1 k,
          trace (A ^ j) * charpolyDescendingCoeff A (k - j) = 0 := by
  sorry

Informal solution sketch

These are Newton's identities relating the power sums pⱼ = tr(Aʲ) (sums of j-th powers of eigenvalues) to the elementary symmetric functions eₖ that appear, up to sign, as the charpoly coefficients cₖ = (−1)ᵏ eₖ. Prove by the standard generating-function / logarithmic-derivative argument: differentiate log det(X·1 − A) = ∑ log(X − λᵢ), expand 1/(X − λᵢ) as a power series in 1/X to get ∑ⱼ pⱼ X^{−j}, and match coefficients against the derivative of the charpoly to obtain k cₖ + ∑{j=1}^k pⱼ c{k−j} = 0. For k > N the relation is the trace of A^{k−N} times Cayley-Hamilton.

Source

Knill, Some fundamental theorems in mathematics, §220.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: trace_cayley_hamilton_newton
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.