S operators (general S ≥ 0, parameterised by N = 2S : ℕ)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
S operators (general S ≥ 0, parameterised by N = 2S : ℕ)Primary reference: Tasaki, Physics and Mathematics of Quantum Many-Body Systems, §2.1 Problem 2.1.a (p. 15) and solution S.1 (p. 493).
Generic spin-S operators live on Matrix (Fin (N + 1)) (Fin (N + 1)) ℂ, with N = 2S : ℕ (so N = 1 ⇔ S = 1/2, N = 2 ⇔ S = 1). Tracking issue #458 (Tasaki §2.1 P1d’’’ general-S generalisation).
| Lean name | Statement | File |
|---|---|---|
spinSOp3 |
Ŝ^(3) := diag(N/2, N/2 - 1, …, -N/2) for N : ℕ |
Quantum/SpinS/Operators.lean |
spinSOpPlus / spinSOpMinus |
raising/lowering operators with matrix entries √(k·(N − k + 1)) (resp. √((N − k)(k + 1))) on the immediate sub/super-diagonal |
Quantum/SpinS/Operators.lean |
spinSOp1 / spinSOp2 |
Ŝ^(1) := (Ŝ^+ + Ŝ^-) / 2, Ŝ^(2) := (Ŝ^+ − Ŝ^-) / (2 i) |
Quantum/SpinS/Operators.lean |
spinSOp{Plus,Minus}_apply_top / _bottom |
Ŝ^+ annihilates \|N⟩ (highest weight); Ŝ^- annihilates \|0⟩ (lowest weight) — the ladder boundaries |
Quantum/SpinS/Operators.lean |
spinSOp3_commutator_spinSOp{Plus,Minus} |
Cartan relations [Ŝ^{(3)}, Ŝ^+] = Ŝ^+ and [Ŝ^{(3)}, Ŝ^-] = -Ŝ^-: Ŝ^± shift the magnetic quantum number by ±1. Proved entry-wise via Matrix.diagonal_mul / mul_diagonal (β-2 of Issue #458) |
Quantum/SpinS/Algebra.lean |
spinSOp{Plus,Minus}_conjTranspose / spinSOp{1,2,3}_isHermitian |
adjointness (Ŝ^+)ᴴ = Ŝ^-, (Ŝ^-)ᴴ = Ŝ^+, and Hermiticity of Ŝ^{(α)} for α ∈ {1, 2, 3} (β-3 of Issue #458). The ladder adjointness follows from the matrix-entry symmetry; Ŝ^{(1)} and Ŝ^{(2)} use the 1/2 and 1/(2i) self-conjugacy facts |
Quantum/SpinS/Hermitian.lean |
spinSDiagProj / spinSOp3_sub_smul_mul_diagProj / _self_mul_diagProj |
the diagonal projector P_k := diag(δ_{i,k}) and the eigenvalue-action lemma (Ŝ^{(3)} − λ_j • 1) · P_k = (λ_k − λ_j) · P_k, with the annihilation specialisation at j = k (β-4 of Issue #458). Foundation for the Lagrange-interpolation polynomial decomposition: each P_k will be expressed as ∏_{j ≠ k} (Ŝ^{(3)} − λ_j • 1) / (λ_k − λ_j) in a follow-up PR |
Quantum/SpinS/DiagProj.lean |
spinSOp3_mul_diagProj / diagProj_mul_spinSOp3 / spinSOp3_commute_diagProj |
the eigenvalue equation Ŝ^{(3)} · P_k = λ_k · P_k (where λ_k = (N : ℂ)/2 − k), with the symmetric P_k · Ŝ^{(3)} = λ_k · P_k and the resulting commutativity. Both are diagonal-times-diagonal computations (β-5 of Issue #458) |
Quantum/SpinS/Lagrange.lean |
mul_diagProj_apply / diagProj_mul_apply / spinSOp{Plus,Minus}_mul_diagProj_apply |
Column/row selection by the diagonal projector: (A · P_k)[i, j] = A[i, k] if j = k else 0 (and dually for P_k · A). Specialised to Ŝ^± produces off-diagonal matrix units (β-6 of Issue #458) — the building blocks of the polynomial decomposition theorem |
Quantum/SpinS/LadderProj.lean |
spinSOpPlus_mul_diagProj_succ_mul_spinSOpMinus |
Ladder recursion: Ŝ^+ · P_{k+1} · Ŝ^- = (k + 1)(N − k) · P_k. The triple product collapses to a non-zero scalar multiple of P_k. Iterating from the lowest-weight projector P_N (itself a polynomial in Ŝ^{(3)}) yields every diagonal projector as a polynomial in {1̂, Ŝ^{(α)}} (β-7 of Issue #458) |
Quantum/SpinS/LadderRecursion.lean |
spinSOpPlus_mul_diagProj_first / spinSOpMinus_mul_diagProj_last |
Ladder boundaries: Ŝ^+ · P_0 = 0 (top of ladder) and Ŝ^- · P_N = 0 (bottom). The first/last columns of Ŝ^± vanish, so multiplication by P_{0/N} (which selects that column) gives 0. Terminate the recursion at the highest- and lowest-weight projectors (β-8 of Issue #458) |
Quantum/SpinS/LadderBoundary.lean |
spinSDiagProj_isHermitian / sum_spinSDiagProj_eq_one |
Hermiticity of each P_k, and the resolution of the identity Σ_k P_k = 1. The latter is the cornerstone for the matrix-unit decomposition: combined with the off-diagonal matrix units (β-6, β-7), gives every matrix in M_{N+1}(ℂ) (β-9 of Issue #458) |
Quantum/SpinS/DiagProjProperties.lean |
spinSOpPlus_mul_diagProj_succ_eq_single / spinSOpMinus_mul_diagProj_eq_single |
Off-diagonal matrix-unit decomposition: Ŝ^+ · P_{i+1} = √((i+1)(N−i)) · E_{i, i+1} and Ŝ^- · P_i = √((N−i)(i+1)) · E_{i+1, i}, where E_{a, b} := Matrix.single a b 1 is the (a, b) matrix unit (β-10 of Issue #458). These are the simplest off-diagonal matrix units expressible via Ŝ^± ladder action on diagonal projectors |
Quantum/SpinS/OffDiagUnit.lean |
spinSOp3_sq_eq_diagonal |
(Ŝ^{(3)})² = diag((N/2 − i)²). Step toward the Casimir identity (Ŝ^{(1)})² + (Ŝ^{(2)})² + (Ŝ^{(3)})² = (N(N+2)/4) · 1 for general spin (β-11 of Issue #458) |
Quantum/SpinS/Op3Square.lean |
spinSOpPlus_mul_spinSOpMinus_eq_diagonal |
Ŝ^+ · Ŝ^- = diag((i + 1)(N − i)). The product is diagonal because Ŝ^+[i, l] · Ŝ^-[l, j] is non-zero only when l = i + 1 = j + 1, forcing i = j. Combined with the analogous Ŝ^- · Ŝ^+ and (Ŝ^{(3)})², this assembles the Casimir identity (β-12 of Issue #458) |
Quantum/SpinS/PlusMinusDiag.lean |
spinSOpMinus_mul_spinSOpPlus_eq_diagonal |
Ŝ^- · Ŝ^+ = diag(i · (N − i + 1)). Symmetric to β-12 with Ŝ^± swapped (β-13 of Issue #458) |
Quantum/SpinS/MinusPlusDiag.lean |
spinSOp1_sq_add_spinSOp2_sq / spinSOp_total_squared |
Casimir identity for general spin-S: (Ŝ^{(1)})² + (Ŝ^{(2)})² + (Ŝ^{(3)})² = (N(N+2)/4) · 1, equivalent to S(S+1) · 1 for S = N/2. Proves the irreducible spin-S representation has Casimir eigenvalue S(S+1) (Schur’s lemma). The intermediate identity (Ŝ^{(1)})² + (Ŝ^{(2)})² = (1/2)(Ŝ^+ · Ŝ^- + Ŝ^- · Ŝ^+) is proved using module (β-14 of Issue #458) |
Quantum/SpinS/Casimir.lean |
spinSOp3_mulVec_basis |
spin-S eigenstate equation Ŝ^{(3)} · \|k⟩ = (N/2 − k) · \|k⟩, where \|k⟩ := Pi.single k 1 is the k-th unit basis vector of (Fin (N + 1) → ℂ) (β-15 of Issue #458) |
Quantum/SpinS/Eigenstates.lean |
spinSOpPlus_mulVec_basis / spinSOpMinus_mulVec_basis |
Ladder action on basis vectors: Ŝ^+ · \|k⟩ = √(k(N − k + 1)) · \|k − 1⟩ for k ≥ 1, and Ŝ^- · \|k⟩ = √((N − k)(k + 1)) · \|k + 1⟩ for k ≤ N − 1. The standard SU(2) ladder relations on the magnetic-quantum-number basis (β-16 of Issue #458) |
Quantum/SpinS/LadderStates.lean |
spinSOp_total_squared_mulVec_basis |
Casimir eigenvalue on basis: (Ŝ)² · \|k⟩ = (N(N+2)/4) · \|k⟩. Direct consequence of (Ŝ)² = (N(N+2)/4) · 1 (β-14) — every basis vector has the universal Casimir eigenvalue, reflecting that the spin-S representation is a single irreducible (Schur) (β-17 of Issue #458) |
Quantum/SpinS/CasimirEigenvalue.lean |
spinSOp{1,2,3,Plus,Minus}_commute_total_squared |
Casimir invariance: each Ŝ^{(α)} and Ŝ^± commutes with the Casimir (Ŝ)² = (N(N+2)/4) · 1. Direct consequence of the scalar nature of the Casimir (β-18 of Issue #458) |
Quantum/SpinS/CasimirInvariance.lean |
spinSOpPlus_commutator_spinSOpMinus |
Third Cartan relation: [Ŝ^+, Ŝ^-] = 2 · Ŝ^{(3)}. Combines β-12 (Ŝ^+ · Ŝ^- = diag((i + 1)(N − i))) and β-13 (Ŝ^- · Ŝ^+ = diag(i (N − i + 1))); the difference (i+1)(N-i) − i(N-i+1) = N − 2i = 2(N/2 − i) matches 2 · Ŝ^{(3)} (β-19 of Issue #458) |
Quantum/SpinS/Cartan3.lean |
spinSOp1_commutator_spinSOp2 |
Cyclic SU(2) commutator [Ŝ^{(1)}, Ŝ^{(2)}] = i · Ŝ^{(3)}. Derived from the Cartan relations by algebraic manipulation through Ŝ^{(1)} = (Ŝ^+ + Ŝ^-)/2 and Ŝ^{(2)} = (Ŝ^+ − Ŝ^-)/(2i): (P+Q)(P-Q) − (P-Q)(P+Q) = -2[P, Q] = -4 Ŝ^{(3)}, then scalar simplification -1/I = I (β-20 of Issue #458) |
Quantum/SpinS/CyclicCommutator.lean |
spinSOp2_commutator_spinSOp3 |
Cyclic SU(2) commutator [Ŝ^{(2)}, Ŝ^{(3)}] = i · Ŝ^{(1)}. Derived from Cartan β-2 ([Ŝ^{(3)}, Ŝ^±] = ±Ŝ^±) via Ŝ^{(2)} = (Ŝ^+ − Ŝ^-)/(2i): the commutator reduces to (1/(2i)) (-Ŝ^+ − Ŝ^-) = (-1/(2i)) · 2 Ŝ^{(1)} = i · Ŝ^{(1)} (β-21 of Issue #458) |
Quantum/SpinS/CyclicCommutator.lean |
spinSOp3_commutator_spinSOp1 |
Cyclic SU(2) commutator [Ŝ^{(3)}, Ŝ^{(1)}] = i · Ŝ^{(2)}. Derived from Cartan β-2 via Ŝ^{(1)} = (Ŝ^+ + Ŝ^-)/2: the commutator reduces to (1/2) (Ŝ^+ − Ŝ^-) = (1/2) · (2i) · Ŝ^{(2)} = i · Ŝ^{(2)}. Together with β-20 and β-21 this completes the standard SU(2) commutator algebra (Tasaki eq. (2.1.1)) for spin-S operators (β-22 of Issue #458) |
Quantum/SpinS/CyclicCommutator.lean |
spinSDiagProj_mul_self / spinSDiagProj_mul_of_ne |
Idempotence and orthogonality of the diagonal projectors P_k = |k⟩⟨k|: P_k · P_k = P_k and P_i · P_j = 0 for i ≠ j. Combined with β-9 (∑_k P_k = 1) this gives the spectral decomposition of the identity for Ŝ^{(3)} (β-23 of Issue #458) |
Quantum/SpinS/DiagProjOrtho.lean |
aeval_diagonal |
Polynomial evaluation at a diagonal matrix: aeval (Matrix.diagonal v) p = Matrix.diagonal (fun i => p.eval (v i)). Foundational lemma for the Lagrange-interpolation step (β-25+) — lets us pull a polynomial in Ŝ^{(3)} (a diagonal matrix) through to its scalar action on each diagonal entry. Proof by Polynomial.induction_on' on monomials and addition (β-24 of Issue #458) |
Quantum/SpinS/AevalDiagonal.lean |
spinSDiagProj_eq_lagrange_aeval |
Lagrange-interpolation formula for P_k: P_k = aeval (Ŝ^{(3)}) (Lagrange.basis Finset.univ (spinSOp3Eigen N) k), equivalently P_k = ∏_{j ≠ k} (Ŝ^{(3)} − λ_j • 1)/(λ_k − λ_j) with λ_j = (N : ℂ)/2 − j.val. Combines β-24 (aeval of diagonal) with mathlib’s Lagrange.eval_basis_self / eval_basis_of_ne. Each diagonal projector is therefore a polynomial in Ŝ^{(3)}, which combined with β-9 (∑ P_k = 1) gives an explicit polynomial decomposition of 1̂ (β-25 of Issue #458) |
Quantum/SpinS/LagrangeFormula.lean |
spinSOpPlus_eq_one_add_I_smul_two / spinSOpMinus_eq_one_sub_I_smul_two |
Inversion of the Cartesian definition: Ŝ^+ = Ŝ^{(1)} + i · Ŝ^{(2)} and Ŝ^- = Ŝ^{(1)} − i · Ŝ^{(2)}. The defining identities Ŝ^{(1)} = (1/2)(Ŝ^+ + Ŝ^-), Ŝ^{(2)} = (1/(2i))(Ŝ^+ − Ŝ^-) invert to express the ladder operators as linear combinations of the Hermitian Cartesian spin operators (β-26 of Issue #458) |
Quantum/SpinS/PMAsOneTwo.lean |
spinSDiagProj_mem_adjoin_spinSOp3 / spinSDiagProj_mem_adjoin |
Diagonal projectors live in the algebra generated by the spin operators: P_k ∈ Algebra.adjoin ℂ {Ŝ^{(3)}} (and a fortiori P_k ∈ Algebra.adjoin ℂ {Ŝ^{(1)}, Ŝ^{(2)}, Ŝ^{(3)}}). Promotes the Lagrange-interpolation formula (β-25) from “polynomial-evaluation” form to “subalgebra-membership” form via Algebra.adjoin_singleton_eq_range_aeval (β-27 of Issue #458) |
Quantum/SpinS/ProjMemAdjoin.lean |
spinSOpPlus_mem_adjoin / spinSOpMinus_mem_adjoin |
Ladder operators live in Algebra.adjoin ℂ {Ŝ^{(α)}}: Ŝ^+, Ŝ^- ∈ Algebra.adjoin ℂ {Ŝ^{(1)}, Ŝ^{(2)}, Ŝ^{(3)}}. Direct consequence of β-26 (Ŝ^± = Ŝ^{(1)} ± i · Ŝ^{(2)}) and the fact that subalgebras are closed under ℂ-linear combinations (β-28 of Issue #458) |
Quantum/SpinS/PMMemAdjoin.lean |
single_succ_mem_adjoin / single_succ_swap_mem_adjoin |
Immediate-neighbor matrix units live in Algebra.adjoin ℂ {Ŝ^{(α)}}: E_{i, i+1}, E_{i+1, i} ∈ Algebra.adjoin ℂ {Ŝ^{(1)}, Ŝ^{(2)}, Ŝ^{(3)}}. Combines β-10 (Ŝ^+ · P_{i+1} = √((i+1)(N-i)) · E_{i, i+1}) with β-27 (P_k ∈ adjoin) and β-28 (Ŝ^± ∈ adjoin); the ladder coefficient is non-zero on the valid range and the subalgebra is closed under multiplication and scalar smul. Step toward expressing every matrix unit as a polynomial in {Ŝ^{(α)}} (β-29 of Issue #458) |
Quantum/SpinS/NeighborUnitAdjoin.lean |
single_offset_succ_mem_adjoin / single_offset_succ_swap_mem_adjoin |
Arbitrary stride-(k+1) matrix units live in Algebra.adjoin ℂ {Ŝ^{(α)}}: E_{i, i+(k+1)}, E_{i+(k+1), i} ∈ Algebra.adjoin ℂ {Ŝ^{(α)}} for any k. Induction on k: base case is β-29; inductive step chains via Matrix.single_mul_single_same (E_{i,j} · E_{j,k} = E_{i,k}) (β-30 of Issue #458) |
Quantum/SpinS/OffsetUnitAdjoin.lean |
matrix_single_mem_adjoin |
Every matrix unit E_{i,j} lives in Algebra.adjoin ℂ {Ŝ^{(α)}}. Three-case split: i = j reduces to β-27 via Matrix.diagonal_single (E_{i,i} = P_i); i.val < j.val is β-30 upper; j.val < i.val is β-30 lower. Last building block before the spanning theorem (β-31 of Issue #458) |
Quantum/SpinS/AllUnitsAdjoin.lean |
matrix_mem_adjoin / spinS_adjoin_eq_top |
🎯 Tasaki §2.1 Problem 2.1.a (P1d’’’) general-S: every operator on the (2S+1)-dimensional spin-S Hilbert space ℂ^{N+1} is a polynomial in {1̂, Ŝ^{(1)}, Ŝ^{(2)}, Ŝ^{(3)}}. Equivalently, Algebra.adjoin ℂ {Ŝ^{(1)}, Ŝ^{(2)}, Ŝ^{(3)}} = ⊤. Proof: every matrix unit E_{i,j} ∈ adjoin (β-31), so by the entry-wise decomposition M = ∑_{i,j} M_{i,j} • E_{i,j} (Matrix.matrix_eq_sum_single) and the linearity of the subalgebra, every matrix is in the adjoin (β-32 of Issue #458) |
Quantum/SpinS/SpanningTheorem.lean |
ManyBodyOpS / onSiteS / spinSSiteOp{1,2,3,Plus,Minus} |
Multi-site spin-S operator space indexed by configurations σ : Λ → Fin (N + 1), with the site-embedded operator onSiteS i A acting as A on site i and as the identity elsewhere; site-specialised Ŝ_i^{(α)}, Ŝ_i^±. Hermiticity preservation onSiteS_isHermitian lifts from single-site to multi-site (Tasaki §2.5 Phase B-β β-3a, Issue #412) |
Quantum/SpinS/MultiSiteCore.lean + Quantum/SpinS/MultiSite.lean |
← S = 1 matrix representations (Tasaki §2.1 eq. (2.1.9)) · Catalogue · Basis states and raising/lowering (Tasaki §2.1) →