Interim authority. This lossless catalogue chunk remains authoritative for formalization status and capstone identification until Issue #5228. The version 1 JSON catalogue is still a non-authoritative prototype.
Interim catalogue › Spin foundations and Tasaki Chapter 2
Primary reference: Tasaki, Physics and Mathematics of Quantum Many-Body Systems, §2.1 eq. (2.1.9), p. 15.
| Lean name | Statement | File |
|---|---|---|
spinOneOp{1,2,3} |
3×3 matrix definitions (Tasaki (2.1.9)) | Quantum/SpinOne.lean |
spinOneOp{1,2,3}_isHermitian |
Hermiticity | Quantum/SpinOne.lean |
spinOneOp1_commutator_spinOneOp2 etc. |
[Ŝ^(α), Ŝ^(β)] = i · Ŝ^(γ) (S = 1) |
Quantum/SpinOne.lean |
spinOne_total_spin_squared |
Σ (Ŝ^(α))² = 2 · I, i.e. S(S+1) with S = 1 |
Quantum/SpinOne.lean |
← Polynomial-basis decomposition for S = 1 (Tasaki §2.1 Problem 2.1.a, S = 1) · Catalogue · Spin-S operators (general S ≥ 0, parameterised by N = 2S : ℕ) →