R^(α)_θ (general θ, Tasaki §2.1 eq. (2.1.11))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^(α)_θ (general θ, Tasaki §2.1 eq. (2.1.11))| Lean name | Statement | File |
|---|---|---|
rot3D{1,2,3} θ |
3×3 real rotation matrices by angle θ about each axis | Quantum/Rotation3D.lean |
rot3D{1,2,3}_zero |
R^(α)_0 = 1 |
Quantum/Rotation3D.lean |
rot3D{1,2,3}_pi |
R^(α)_π from general formula matches explicit π-rotation |
Quantum/Rotation3D.lean |
← Spin-1/2 rotation operators (Tasaki §2.1 eq. (2.1.26)) · Catalogue · Z₂ × Z₂ representation (Tasaki §2.1 eqs. (2.1.27)-(2.1.34)) →