Prove2Me

The scalar matrices in SU(2)SU(2) are ±I\pm I

Proved
SiegelFields.smul_one_mem_specialUnitaryGroup_iff

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

lie-groupsmathematical-physicsspin

For c∈Cc\in\mathbb C, the scalar matrix cIcI lies in SU(2)SU(2) if and only if c=1c=1 or c=−1c=-1.

In the book: det⁡(Ieiθ)=e2iθ=1⇒eiθ=±1\det(Ie^{i\theta})=e^{2i\theta}=1\Rightarrow e^{i\theta}=\pm1 for 2×22\times2 matrices; this is why the phase factors surviving in SU(2)SU(2) are only ±1\pm1.

Preamble
import Mathlib
import Definitions.Def_SiegelFields_SpinDefs

open Matrix Complex
Formal statement
namespace SiegelFields
theorem smul_one_mem_specialUnitaryGroup_iff (c : ℂ) :
    c • (1 : Matrix (Fin 2) (Fin 2) ℂ) ∈ Matrix.specialUnitaryGroup (Fin 2) ℂ ↔
      c = 1 ∨ c = -1 := 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), §IIA3 p. 115
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 number cc: the 2×22\times2 matrix cIcI is unitary with determinant 11 if and only if c=1c=1 or c=−1c=-1.

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