R^(α)_π (Tasaki §2.1 eq. (2.1.28))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
R^(α)_π (Tasaki §2.1 eq. (2.1.28))Primary reference: Tasaki, Physics and Mathematics of Quantum Many-Body Systems, §2.1 eqs. (2.1.27)-(2.1.28), p. 18 and Problem 2.1.f.
| Lean name | Statement | File |
|---|---|---|
rot3D{1,2,3}Pi |
3×3 real orthogonal π-rotation matrices | Quantum/Rotation3D.lean |
rot3D{1,2,3}Pi_sq |
(R^(α)_π)² = 1 |
Quantum/Rotation3D.lean |
rot3D{1,2,3}Pi_mul_rot3D{2,3,1}Pi |
R^(α)_π · R^(β)_π = R^(γ)_π (cyclic, Problem 2.1.f) |
Quantum/Rotation3D.lean |
rot3D{1,2,3}Pi_comm_* |
distinct-axis R^(α)_π and R^(β)_π commute |
Quantum/Rotation3D.lean |
← Z₂ × Z₂ representation (Tasaki §2.1 eqs. (2.1.27)-(2.1.34)) · Catalogue · Pauli-basis decomposition (Tasaki §2.1 Problem 2.1.a, S = 1/2) →