lattice-system

Legacy catalogue: Z₂ × Z₂ representation (Tasaki §2.1 eqs. (2.1.27)-(2.1.34))

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

Z₂ × Z₂ representation (Tasaki §2.1 eqs. (2.1.27)-(2.1.34))

The Z₂ × Z₂ structure is proved across files:

• S = 1/2 (projective, eq. (2.1.31)): spinHalfRot*_pi_sq = -1, anticommutation, products.
• S = 1 (genuine, eq. (2.1.27)): spinOnePiRot*_sq = 1, commutation.

See Quantum/Z2Z2.lean for the unified documentation.

---

← 3D rotation matrices R^(α)_θ (general θ, Tasaki §2.1 eq. (2.1.11)) · Catalogue · 3D rotation matrices R^(α)_π (Tasaki §2.1 eq. (2.1.28)) →