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 eqs. (2.1.1), (2.1.7), (2.1.8), pp. 13-15.
| Lean name | Statement | File |
|---|---|---|
spinHalfOp{1,2,3} |
Ŝ^(α) := σ^(α) / 2 (Tasaki (2.1.7)) |
Quantum/SpinHalf.lean |
pauliX_eq_two_smul_spinHalfOp1 etc. |
σ^(α) = 2 · Ŝ^(α) (Tasaki (2.1.8)) |
Quantum/SpinHalf.lean |
spinHalfOp1_isHermitian etc. |
Ŝ^(α) is Hermitian |
Quantum/SpinHalf.lean |
spinHalfOp1_mul_self etc. |
(Ŝ^(α))² = (1/4) · I |
Quantum/SpinHalf.lean |
spinHalfOp1_anticomm_spinHalfOp2 etc. |
anticommutation at α ≠ β |
Quantum/SpinHalf.lean |
spinHalfOp1_commutator_spinHalfOp2 etc. |
[Ŝ^(α), Ŝ^(β)] = i · Ŝ^(γ) (Tasaki (2.1.1)) |
Quantum/SpinHalf.lean |
spinHalf_total_spin_squared |
Σ (Ŝ^(α))² = (3/4) · I, i.e. S(S+1) with S=1/2 |
Quantum/SpinHalf.lean |
← Single-site Pauli operators · Catalogue · Spin-1/2 rotation operators (Tasaki §2.1 eq. (2.1.26)) →