Identities with $C$ : $MCM^TC=I\det M$ , $M+CM^TC=I\operatorname{tr}M$ , and $\operatorname{tr}V=0\iff (VC)^T=VC$

Proved

SiegelFields.matC_identities

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

lie-groupsmathematical-physicsspin

Let $C=\begin{pmatrix}0&-i\\ i&0\end{pmatrix}$ . For every complex $2\times2$ matrix $M$ :

$MCM^TC=(\det M)\,I$ ;
$M+CM^TC=(\operatorname{tr}M)\,I$ ;
$\operatorname{tr}M=0$ if and only if $(MC)^T=MC$ .

The first gives the inverse $M^{-1}=CM^TC(\det M)^{-1}$ ; the third says tracelessness of $V$ is equivalent to symmetry of $VC$ .

Preamble

import Mathlib
import Definitions.Def_SiegelFields_SpinDefs

open Matrix Complex

Formal statement

namespace SiegelFields
theorem matC_identities (M : Matrix (Fin 2) (Fin 2) ℂ) :
    M * matC * Mᵀ * matC = M.det • (1 : Matrix (Fin 2) (Fin 2) ℂ) ∧
      M + matC * Mᵀ * matC = trace M • (1 : Matrix (Fin 2) (Fin 2) ℂ) ∧
      (trace M = 0 ↔ (M * matC)ᵀ = M * matC) := 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 pp. 111–112

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 complex $2\times2$ matrix $M$ (no hypothesis), with $C=\begin{pmatrix}0&-i\\ i&0\end{pmatrix}$ and $M^T$ the (plain, not conjugate) transpose: (1) $MCM^TC=(\det M)\,I$ ; (2) $M+CM^TC=(\operatorname{tr}M)\,I$ ; (3) $\operatorname{tr}M=0$ holds if and only if the transpose of $MC$ equals $MC$ .

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

Identities with CCC: MCMTC=Idet⁡MMCM^TC=I\det MMCMTC=IdetM, M+CMTC=Itr⁡MM+CM^TC=I\operatorname{tr}MM+CMTC=ItrM, and tr⁡V=0 ⟺ (VC)T=VC\operatorname{tr}V=0\iff (VC)^T=VCtrV=0⟺(VC)T=VC

Identities with $C$ : $MCM^TC=I\det M$ , $M+CM^TC=I\operatorname{tr}M$ , and $\operatorname{tr}V=0\iff (VC)^T=VC$