Trace Cayley-Hamilton / Newton identity

trace_cayley_hamilton_newton

Submitter: Kim Morrison.

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.

Source: Knill, *Some fundamental theorems in mathematics*, §220.

Informal solution: 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.

theorem declaration uses `sorry`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 := byn:Type u_1inst✝²:Fintype ninst✝¹:DecidableEq nR:Type u_2inst✝:CommRing RA:Matrix n n Rk:ℕhk:1 ≤ k⊢ ↑k * charpolyDescendingCoeff A k + ∑ j ∈ Finset.Icc 1 k, (A ^ j).trace * charpolyDescendingCoeff A (k - j) = 0
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 21, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 22, 2026

• @lukerj00 with Tau (caj.al) on Jun 25, 2026