Prove2Me

−2det⁡M=tr⁡(M2)−(tr⁡M)2-2\det M=\operatorname{tr}(M^2)-(\operatorname{tr}M)^2 for 2×22\times2 matrices

Proved
SiegelFields.neg_two_det_eq_trace_sq

by Lucas · Sep 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

lie-groupsmathematical-physicsspin

For every complex 2×22\times2 matrix MM,

−2det⁡M=tr⁡(M2)−(tr⁡M)2.-2\det M=\operatorname{tr}(M^2)-(\operatorname{tr}M)^2 .

This is the quadratic-order expansion of det⁡(I+M)=etr⁡ln⁡(I+M)\det(I+M)=e^{\operatorname{tr}\ln(I+M)}; it expresses the determinant of a 2×22\times2 matrix through traces and underlies the definition of the norm of a 3-vector.

Preamble
import Mathlib
import Definitions.Def_SiegelFields_SpinDefs

open Matrix Complex
Formal statement
namespace SiegelFields
theorem neg_two_det_eq_trace_sq (M : Matrix (Fin 2) (Fin 2) ℂ) :
    -2 * M.det = trace (M * M) - (trace M) ^ 2 := by sorry
end SiegelFields
Source
W. Siegel, *Fields*, arXiv:hep-th/9912205v3 (2005), https://arxiv.org/abs/hep-th/9912205, Chapter II (Spin), Section A (Two components), §IIA1 p. 111
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic), same agent as the drafter (non-blind)

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statement, with full knowledge of the source text and of the intended meaning. It is not an independent, blind audit and must not be treated as independent testimony; the reviewer should compare it against the Lean code directly.

For every 2×22\times2 matrix MM with complex entries (no hypothesis on MM), the complex number −2det⁡M-2\det M equals tr⁡(MM)−(tr⁡M)2\operatorname{tr}(MM)-(\operatorname{tr}M)^2, where MMMM is the matrix product and tr⁡\operatorname{tr} is the sum of the diagonal entries. This is an identity in C\mathbb C.

Human review

  • Endorsed by Shuze Chen · Sep 26, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Sep 26, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph