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
| Lean name | Statement | File |
|—|—|—|
| magSumS_neelConfigOfS_complement / magnetization_neelConfigOf_complement | Sublattice-swap symmetry of Néel magnetization: magSumS (neelConfigOfS (¬A) N) = \|A\|·N (spin-S) and magnetization Λ (neelConfigOf (¬A)) = \|¬A\| - \|A\| (spin-1/2). The complement Néel configuration sits in the opposite magnetization sector to the original (γ-4 step 169) | Quantum/SpinS/SublatticeCasimirNeelCore.lean and Quantum/MarshallLiebMattis/SublatticeCasimirNeelCore.lean (PR #1216) |
| heisenbergHamiltonianOnGraphS_apply_diag_neel_bipartiteCompleteGraph and state-level form | Specialization to bipartiteCompleteGraphOf A (spin-S): the Heisenberg-on-graph Néel expectation on the canonical complete bipartite graph (Λ, A) (every edge crosses sublattices). One-line corollary of γ-4 step 166 via the existing bipartiteCompleteGraphOf_adj_sublattice_ne (γ-4 step 170) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1217) |
| neelStateOfS_complement_orthogonal / neelStateOf_complement_orthogonal and neelConfigOfS_ne_complement / neelConfigOf_ne_complement | Néel-complement orthogonality: <Φ_Néel(A) \| Φ_Néel(¬A)> = 0 when Λ non-empty (and 0 < N for spin-S). The two Néel states are basis vectors at distinct configurations (the inequality is witnessed by any vertex x where the sublattice-swap exchanges the spin label), hence orthogonal (γ-4 step 171) | Quantum/SpinS/SublatticeCasimirNeelCore.lean and Quantum/MarshallLiebMattis/SublatticeCasimirNeelCore.lean (PR #1218) |
| neelStateOfS_complement_pair_independent / neelStateOf_complement_pair_independent | Néel-complement linear independence: c1 • Φ_Néel(A) + c2 • Φ_Néel(¬A) = 0 → c1 = c2 = 0 when Λ non-empty (and 0 < N for spin-S). Combines γ-4 step 171 (orthogonality) with norm-squared = 1 by taking <Φ_Néel(A) \| ·> and <Φ_Néel(¬A) \| ·> of the relation. The pair spans a 2-dimensional subspace of the multi-site Hilbert space (γ-4 step 172) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean and Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean (PR #1219) |
| neelStateOfS_mem_magSubspaceS and neelStateOfS_complement_mem_magSubspaceS / neelStateOf_complement_mem_magnetizationSubspace | Magnetization subspace membership of Néel: Φ_Néel(A) ∈ magSubspaceS ((|A|-|¬A|)·N/2) (spin-S, basic) and Φ_Néel(¬A) ∈ magSubspaceS ((|¬A|-|A|)·N/2) — the complement Néel sits in the opposite-sign magnetization sector. Spin-1/2 mirror also added (γ-4 step 176) | Quantum/SpinS/SublatticeCasimirNeelCore.lean (the spin-1/2 mirror lived in Quantum/MarshallLiebMattis/SublatticeCasimirNeelMagnetization.lean, moved there when refactor #46, PR #2982 split it out of Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean, and was deleted in PR #3919 (bulk orphan-module deletion)) (PR #1223) |
| magSubspaceS_nontrivial_via_neel and neelStateOfS_span_le_magSubspaceS | Spin-S magnetization subspace non-triviality: magSubspaceS Λ N M_neel ≠ ⊥ (witnessed by non-zero Néel) and span ℂ {Φ_Néel} ≤ magSubspaceS. Spin-S mirrors of magnetizationSubspace_nontrivial_via_neel and neelStateOf_span_le_magnetizationSubspace (γ-4 step 177) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (PR #1224) |
| magSubspaceS_complement_nontrivial_via_neel / magnetizationSubspace_complement_nontrivial_via_neel | Complement magnetization subspace non-triviality: the opposite-sign sector (|¬A|-|A|)·N/2 (or (|¬A|-|A|)/2 for spin-1/2) is non-trivial, witnessed by the non-zero Φ_Néel(¬A). Spin-S and spin-1/2 (γ-4 step 178) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (the spin-1/2 mirror lived in Quantum/MarshallLiebMattis/SublatticeCasimirNeelMagnetization.lean, moved there when refactor #46, PR #2982 split it out of Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean, and was deleted in PR #3919 (bulk orphan-module deletion)) (PR #1225) |
| neelStateOfS_ne_complement / neelStateOf_ne_complement (state-level) | State-level Néel ≠ complement Néel: the two Néel states are distinct in the Hilbert space when Λ non-empty (and 0 < N for spin-S). Direct from orthogonality + norm-squared = 1 (γ-4 step 179) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean and Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean (PR #1226) |
| neelStateOfS_complement_allAligned_triple_{linearIndependent,finrank_span} and spin-1/2 mirrors neelStateOf_complement_basisVec_triple_{linearIndependent,finrank_span} | Complement-Néel triple LinearIndependent + finrank=3: LinearIndependent ℂ ![Φ_⊤, Φ_⊥, Φ_Néel(¬A)] and the corresponding finrank, spin-S and spin-1/2 (γ-4 step 192) | Quantum/SpinS/SublatticeCasimirNeel.lean and Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean (PR #1239) |
| neelStateOfS_complement_span_le_magSubspaceS / neelStateOf_complement_span_le_magnetizationSubspace | Complement Néel singleton span ⊆ opposite-sign magnetization sector: span ℂ {Φ_Néel(¬A)} ≤ magSubspace ((|¬A|-|A|)·N/2) (spin-S and spin-1/2). Counterpart of the original-A version (γ-4 step 194) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (the spin-1/2 mirror lived in Quantum/MarshallLiebMattis/SublatticeCasimirNeelMagnetization.lean, moved there when refactor #46, PR #2982 split it out of Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean, and was deleted in PR #3919 (bulk orphan-module deletion)) (PR #1241) |
| allAlignedStateS_span_le_magSubspaceS | All-aligned singleton span ⊆ magnetization subspace: span ℂ {allAlignedStateS V N c} ≤ magSubspaceS V N (|V|·N/2 - |V|·c.val). Direct from allAlignedStateS_mem_magSubspaceS (γ-4 step 195) | Quantum/SpinS/AllAlignedStateMagSubspace.lean (PR #1242) |
| neelStateOfS_pair_span_le_magSubspaceS_sup / neelStateOf_pair_span_le_magnetizationSubspace_sup | Néel-pair span ⊆ supremum of opposite-sign magnetization sectors: span ℂ {Φ_Néel(A), Φ_Néel(¬A)} ≤ magSubspace M_pos ⊔ magSubspace M_neg. Direct via Submodule.mem_sup_left/right from γ-4 step 176 + 194; the supremum is a true direct sum precisely when the sectors are distinct (i.e. \|A\| ≠ \|¬A\| and 0 < N) (γ-4 step 197) | Quantum/SpinS/SublatticeCasimirNeelExpectations.lean (the spin-1/2 mirror lived in Quantum/MarshallLiebMattis/SublatticeCasimirNeelMagnetization.lean, moved there when refactor #46, PR #2982 split it out of Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean, and was deleted in PR #3919 (bulk orphan-module deletion)) (PR #1244) |
| bipartiteCompleteGraphOf_edgeFinset_card and neelStateOfS_heisenbergHamiltonianOnGraphS_expectation_bipartiteCompleteGraph_closed | Edge count + closed-form Néel expectation on bipartiteCompleteGraphOf A: #G.edgeFinset = \|A\| · \|¬A\| (via couplingOf_sum + bipartiteCoupling_sum + linear_combination + omega); <Φ_Néel \| H_G \| Φ_Néel> = -J · \|A\| · \|¬A\| · N²/2 (γ-4 step 198) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1245) |
| heisenbergToyHamiltonianS_eq_heisenbergHamiltonianOnGraphS_bipartiteCompleteGraph | Identification: heisenbergToyHamiltonianS A N = heisenbergHamiltonianOnGraphS (bipartiteCompleteGraphOf A) 1 N. The toy Hamiltonian is exactly the unit-coupling Heisenberg on the canonical complete bipartite graph (γ-4 step 199) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1246) |
| neelStateOfS_heisenbergHamiltonianOnGraphS_expectation_bipartiteCompleteGraph_re_neg | Strict ℝ-negativity on bipartiteCompleteGraphOf A for real positive J, \|A\| > 0, \|¬A\| > 0, 0 < N: Re <Φ_Néel \| H \| Φ_Néel> < 0. Specializes γ-4 step 168 using γ-4 step 198 edge count (γ-4 step 200) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1247) |
| basisVec_const_totalSpinHalfSquared_expectation | Spin-1/2 constant-state (Ŝ_tot)² expectation: <basisVec(const s) \| (Ŝ_tot)² \| basisVec(const s)> = \|Λ\|·(\|Λ\|+2)/4 for any s : Fin 2 (γ-4 step 201) | Quantum/SpinDot/HamiltonianCore.lean (PR #1248) |
| allAlignedStateS_expectation_totalSpinSOp3_sq (with allAlignedStateS_{zero,last}_expectation_totalSpinSOp3_sq specialisations) | Spin-S (Ŝ_tot^(3))² expectation on the all-aligned state: <Φ_aligned(c) \| (Ŝ_tot^(3))² \| Φ_aligned(c)> = (magEigenvalueS c)²; specialisations c = 0 and c = Fin.last N give (\|V\|·N/2)² (γ-4 step 202) | Quantum/SpinS/AllAlignedStateExpectations.lean (PR #1249) |
| basisVec_const_totalSpinHalfOp3_sq_expectation | Spin-1/2 constant-state (Ŝ_tot^(3))² expectation: <basisVec(const s) \| (Ŝ_tot^(3))² \| basisVec(const s)> = \|Λ\|²/4 for any s : Fin 2. The constant state is an Ŝ_tot^(3)-eigenvector with eigenvalue ±\|Λ\|/2; squaring gives the same \|Λ\|²/4 (γ-4 step 203) | Quantum/SpinDot/HamiltonianCore.lean (PR #1250) |
| basisVec_totalSpinHalfOp3_sq_expectation | Spin-1/2 arbitrary-σ (Ŝ_tot^(3))² expectation: <basisVec σ \| (Ŝ_tot^(3))² \| basisVec σ> = magnetization(σ)²/4 for any σ : Λ → Fin 2. Generalises γ-4 step 203 (constant case has magnetization = ±\|Λ\|) (γ-4 step 204) | Quantum/SpinDot/HamiltonianCore.lean (PR #1251) |
| basisVecS_expectation_totalSpinSOp3_sq | Spin-S arbitrary-σ (Ŝ_tot^(3))² expectation: <basisVecS σ \| (Ŝ_tot^(3))² \| basisVecS σ> = (magEigenvalueS σ)² for any σ : V → Fin (N + 1). Generalises γ-4 step 202 (the all-aligned case σ = allAlignedConfigS V N c) (γ-4 step 205) | Quantum/SpinS/AllAlignedStateExpectations.lean (PR #1252) |
| basisVecS_expectation_totalSpinSOp3 | Spin-S arbitrary-σ linear Ŝ_tot^(3) expectation: <basisVecS σ \| Ŝ_tot^(3) \| basisVecS σ> = magEigenvalueS σ for any σ : V → Fin (N + 1). Generalises the all-aligned c = 0 / c = Fin.last N cases (γ-4 step 206) | Quantum/SpinS/AllAlignedStateExpectations.lean (PR #1253) |
| basisVec_totalSpinHalfOp3_expectation | Spin-1/2 arbitrary-σ linear Ŝ_tot^(3) expectation: <basisVec σ \| Ŝ_tot^(3) \| basisVec σ> = magnetization(σ)/2 for any σ : Λ → Fin 2. Spin-1/2 mirror of γ-4 step 206 (γ-4 step 207) | Quantum/SpinDot/HamiltonianCore.lean (PR #1254) |
| basisVecS_totalSpinSOp3_variance_eq_zero and spin-1/2 mirror basisVec_totalSpinHalfOp3_variance_eq_zero | Ŝ_tot^(3) zero variance on basis states: <(Ŝ_tot^(3))²> − <Ŝ_tot^(3)>² = 0 on basisVecS σ (spin-S) and on basisVec σ (spin-1/2). Direct corollary of steps 205/206 (spin-S) and 204/207 (spin-1/2); witnesses that every basis state is a sharp Ŝ_tot^(3)-eigenstate (γ-4 step 208) | Quantum/SpinS/AllAlignedStateExpectations.lean and Quantum/SpinDot/HamiltonianCore.lean (PR #1255) |
| basisVecS_off_diagonal_totalSpinSOp3 and spin-1/2 mirror basisVec_off_diagonal_totalSpinHalfOp3 | Off-diagonal Ŝ_tot^(3) matrix elements vanish: <basisVecS τ \| Ŝ_tot^(3) \| basisVecS σ> = 0 for τ ≠ σ (spin-S), and analogue for spin-1/2. Witnesses that Ŝ_tot^(3) is diagonal in the computational basis (γ-4 step 209) | Quantum/SpinS/AllAlignedStateExpectations.lean and Quantum/SpinDot/HamiltonianCore.lean (PR #1256) |
| basisVecS_dotProduct_basisVecS_of_ne and spin-1/2 mirror basisVec_dotProduct_basisVec_of_ne | Basis orthogonality: <basisVecS τ \| basisVecS σ> = 0 for τ ≠ σ (spin-S), and analogue for spin-1/2. Companion to the existing diagonal _inner_self (= 1) lemma; together they witness that the computational basis is orthonormal (γ-4 step 210) | Quantum/SpinS/AllAlignedStateExpectations.lean and Quantum/SpinDot/HamiltonianCore.lean (PR #1257) |
| basisVecS_dotProduct_basisVecS and spin-1/2 mirror basisVec_dotProduct_basisVec | Combined δ-form: <basisVecS τ \| basisVecS σ> = if τ = σ then 1 else 0 (and spin-1/2 analogue). Single-statement combination of the diagonal-1 and off-diagonal-0 facts (γ-4 step 211) | Quantum/SpinS/AllAlignedStateExpectations.lean and Quantum/SpinDot/HamiltonianCore.lean (PR #1258) |
| basisVecS_dotProduct_totalSpinSOp3_basisVecS and spin-1/2 mirror basisVec_dotProduct_totalSpinHalfOp3_basisVec | Combined Ŝ_tot^(3) δ-form matrix element: <basisVecS τ \| Ŝ_tot^(3) \| basisVecS σ> = if τ = σ then magEigenvalueS σ else 0 (spin-S); spin-1/2 analogue with M(σ)/2. Single-statement combination of γ-4 step 206/207 (diagonal) and γ-4 step 209 (off-diagonal) (γ-4 step 212) | Quantum/SpinS/AllAlignedStateExpectations.lean and Quantum/SpinDot/HamiltonianCore.lean (PR #1259) |
| basisVecS_dotProduct_totalSpinSOp3_sq_basisVecS and spin-1/2 mirror basisVec_dotProduct_totalSpinHalfOp3_sq_basisVec | Combined (Ŝ_tot^(3))² δ-form matrix element: <basisVecS τ \| (Ŝ_tot^(3))² \| basisVecS σ> = if τ = σ then (magEigenvalueS σ)² else 0 (spin-S); spin-1/2 analogue with (M(σ)/2)². Off-diagonal proven via the Ŝ_tot^(3) eigenvector identity applied twice + basis orthogonality (γ-4 step 213) | Quantum/SpinS/AllAlignedStateExpectations.lean and Quantum/SpinDot/HamiltonianCore.lean (PR #1260) |
| basisVecS_expectation_totalSpinSOp1 / _totalSpinSOp2 | Spin-S transverse Ŝ_tot^(1,2) zero expectation on every basis state: <basisVecS σ \| Ŝ_tot^(1) \| basisVecS σ> = 0 and <basisVecS σ \| Ŝ_tot^(2) \| basisVecS σ> = 0. Direct from per-site basisVecS_expectation_onSiteS_spinSOp{1,2} summed over sites via Matrix.sum_mulVec + dotProduct_sum (γ-4 step 214) | Quantum/SpinS/SingleSiteTransverseMeanZero.lean (PR #1261) |
| basisVec_expectation_totalSpinHalfOp1 / _totalSpinHalfOp2 | Spin-1/2 transverse Ŝ_tot^(1,2) zero expectation on every basis state: <basisVec σ \| Ŝ_tot^(1) \| basisVec σ> = 0 and <basisVec σ \| Ŝ_tot^(2) \| basisVec σ> = 0. Spin-1/2 mirror of γ-4 step 214; per-site uses basisVec_expectation_eq_diagonal + pauliX/Y zero diagonal (γ-4 step 215) | Quantum/SpinDot/Hamiltonian.lean (PR #1262) |
| basisVecS_totalSpinSSquared_expectation_general | Spin-S (Ŝ_tot)² Casimir expectation on arbitrary basisVecS σ: <basisVecS σ \| (Ŝ_tot)² \| basisVecS σ> = \|V\|·N(N+2)/4 + magEigenvalueS(σ)² − Σ_x (N/2 − σx.val)² for any σ : Λ → Fin (N + 1). Spin-S analogue of γ-4 step 216; the per-site sum-of-squares term is the configuration-dependent z-axis squared contribution that doesn’t collapse for spin-S. Spin-1/2 is the special case where the term reduces to constant \|Λ\|/4 (γ-4 step 218) | Quantum/SpinS/SublatticeCasimirNeelBasisVecS.lean (PR #1265) |
| basisVecS_totalSpinSOp12_sq_expectation_general | Spin-S transverse Casimir (Ŝ_tot^(1))² + (Ŝ_tot^(2))² on arbitrary basisVecS σ = \|V\|·N(N+2)/4 − Σ_x (N/2 − σx.val)². Direct corollary of γ-4 step 218 + γ-4 step 205 (magEigenvalueS² cancels). Reduces to \|V\|·N/2 for Néel on balanced bipartite graphs (matches γ-4 step 156) and to \|Λ\|/2 for spin-1/2 (γ-4 step 220) | Quantum/SpinS/SublatticeCasimirNeelBasisVecS.lean (PR #1267) |
| neelConfigOfS_z_eigenvalue_sq_sum | Néel per-site z-eigenvalue squared sum: Σ_x (N/2 − (neelConfigOfS A N x).val)² = \|V\|·(N/2)². Both extremes σx ∈ {0, N} give (N/2)². Bridges γ-4 step 218 (general formula) to existing closed-form Néel Casimir (γ-4 step 221) | Quantum/SpinS/SublatticeCasimirNeelBasisVecS.lean (PR #1268) |
| allAlignedConfigS_z_eigenvalue_sq_sum | AllAligned per-site z-eigenvalue squared sum: Σ_x (N/2 − (allAlignedConfigS V N c x).val)² = \|V\|·(N/2 − c.val)². Trivial direct computation since σx = c constant. Bridges γ-4 step 218 to existing allAlignedStateS_zero_/_last_expectation_totalSpinSSquared (γ-4 step 222) | Quantum/SpinS/AllAlignedStateExpectations.lean (PR #1269) |
| magEigenvalueS_neelConfigOfS | Néel Ŝ_tot^(3) eigenvalue: magEigenvalueS (neelConfigOfS A N) = (\|A\| − \|¬A\|)·N/2. Direct from magSumS_neelConfigOfS (= \|¬A\|·N) and the filter-card decomposition \|V\| = \|A\| + \|¬A\|. Named lemma extracted from inlined computation in neelStateOfS_totalSpinSSquared_expectation_card_Lambda (γ-4 step 224) | Quantum/SpinS/SublatticeCasimirNeelBasisVecS.lean (PR #1271) |
| allAlignedStateS_{zero,last}_totalSpinSSquared_via_general | Spin-S allAligned-up/down Casimir re-derived via general formula: <Φ_⊤ \| (Ŝ_tot)² \| Φ_⊤> = m_max·(m_max+1) (and same for Φ_⊥) where m_max = \|V\|·N/2. Composition of γ-4 step 218 + γ-4 step 222 + magEigenvalueS_allAlignedConfigS + ring. Recovers existing allAlignedStateS_zero_expectation_totalSpinSSquared (γ-4 step 226) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1273) |
| magEigenvalueS_neelConfigOfS_complement | Complement Néel Ŝ_tot^(3) eigenvalue: magEigenvalueS (neelConfigOfS (¬A) N) = (\|¬A\|−\|A\|)·N/2. Sublattice-swap symmetry; complement of γ-4 step 224. Direct corollary by applying γ-4 step 224 to (¬A) (γ-4 step 229) | Quantum/SpinS/SublatticeCasimirNeelBasisVecS.lean (PR #1276) |
| magEigenvalueS_neelConfigOfS_complement_simplified | Cleaner form of γ-4 step 229 with double negation !!A simplified to A via Finset.filter_congr + Bool.not_not: magEigenvalueS (neelConfigOfS (¬A) N) = (\|¬A\|−\|A\|)·N/2 (γ-4 step 230) | Quantum/SpinS/SublatticeCasimirNeelBasisVecS.lean (PR #1277) |
| magEigenvalueS_neelConfigOfS_complement_eq_neg | Negation relation: magEigenvalueS (neelConfigOfS (¬A) N) = −magEigenvalueS (neelConfigOfS A N). Direct from γ-4 step 224 + γ-4 step 230 + ring. The complement Néel sits at the opposite Ŝ_tot^(3) eigenvalue (γ-4 step 231) | Quantum/SpinS/SublatticeCasimirNeelBasisVecS.lean (PR #1278) |
| neelStateOfS_totalSpinSSquared_complement_eq | Spin-S Casimir is sublattice-swap invariant on Néel: <Φ_Néel(¬A)\|(Ŝ_tot)²\|Φ_Néel(¬A)> = <Φ_Néel(A)\|(Ŝ_tot)²\|Φ_Néel(A)>. Direct from γ-4 step 218 + 221 + 231 + ring: magEigenvalueS² is sign-flip invariant; Σ_x m_x² evaluates to \|V\|·(N/2)² for both A and ¬A. Spin-S mirror of γ-4 step 233 (γ-4 step 234) | Quantum/SpinS/SublatticeCasimirNeelBasisVecS.lean (PR #1281) |
| neelStateOfS_totalSpinSOp3_sq_complement_eq | Spin-S (Ŝ_tot^(3))² is sublattice-swap invariant on Néel: <Φ_Néel(¬A)\|(Ŝ_tot^(3))²\|Φ_Néel(¬A)> = <Φ_Néel(A)\|(Ŝ_tot^(3))²\|Φ_Néel(A)>. Direct from γ-4 step 205 + 231 + ring: squared eigenvalue is sign-flip invariant (γ-4 step 235) | Quantum/SpinS/SublatticeCasimirNeelBasisVecS.lean (PR #1282) |
| neelStateOfS_totalSpinSOp12_sq_complement_eq | Spin-S transverse Casimir (Ŝ^1)²+(Ŝ^2)² is sublattice-swap invariant on Néel: equal expectations on Φ_Néel(A) and Φ_Néel(¬A). Both reduce to \|V\|·N/2 via γ-4 step 220 + 221 (γ-4 step 237) | Quantum/SpinS/SublatticeCasimirNeelBasisVecS.lean (PR #1284) |
| neelStateOfS_totalSpinSOp3_complement_eq_neg | Spin-S linear Ŝ_tot^(3) negates under sublattice swap on Néel: <Φ_Néel(¬A)\|Ŝ_tot^(3)\|Φ_Néel(¬A)> = −<Φ_Néel(A)\|Ŝ_tot^(3)\|Φ_Néel(A)>. Direct from γ-4 step 206 + 231 (γ-4 step 239) | Quantum/SpinS/SublatticeCasimirNeelBasisVecS.lean (PR #1286) |
| neelStateOfS_totalSpinSOp{1,2}_expectation | Spin-S Néel transverse linear expectations vanish: <Φ_Néel\|Ŝ_tot^(1,2)\|Φ_Néel> = 0. Trivial corollary of γ-4 step 214 applied to σ = neelConfigOfS A N (γ-4 step 241). Together with γ-4 step 91 (<Ŝ_tot^(3)> = magEigenvalueS_neelConfigOfS), gives the complete per-axis profile (0, 0, (\|A\|−\|¬A\|)·N/2) | Quantum/SpinS/SublatticeCasimirNeel.lean (PR #1288) |
| neelStateOf_totalSpinHalfOp1/2_expectation | Spin-1/2 Néel transverse linear expectations vanish: same as γ-4 step 241 for spin-1/2, derived from γ-4 step 215 (γ-4 step 242) | Quantum/MarshallLiebMattis/SublatticeCasimirNeel.lean (PR #1289) |
The single-cluster Problem 2.5.a modules below are imported from the
build root again after the 2026-05-30 orphan-module sweep had removed
the earlier implementation. The restored concrete tip is
Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean, and the
minimum-eigenvalue bridge in Quantum/SpinS/SingleClusterHamiltonianMin.lean
keeps the abstract Hamiltonian, energy hygiene, concrete
dimer/trimer/quartet/pentamer eigenvalue formulas, and variational
upper/lower-bound consumers live in the default Lean build
(PR #4032; PR #4033; PR #4034; PR #4035; PR #4036).
| Lean name | Statement | File |
|—|—|—|
| singleClusterHamiltonianS | Single-cluster (star-graph) Heisenberg Hamiltonian (Tasaki Problem 2.5.a, p. 38): H = Σ_{j=1}^z Ŝ_0 · Ŝ_j on Fin (z + 1) with central vertex 0 and z leaves. Ground-state energy −S(1 + zS) (γ-5 step 243) | Quantum/SpinS/SingleClusterHamiltonianCore.lean (PR #1290) |
| singleClusterHamiltonianS_isHermitian | Hermiticity of the single-cluster Heisenberg Hamiltonian. Sum of Hermitian spinSDot 0 j N over j ∈ univ.erase 0 (γ-5 step 244) | Quantum/SpinS/SingleClusterHamiltonianCore.lean (PR #1291) |
| singleClusterHamiltonianS_zero_z | Edge case z = 0: singleClusterHamiltonianS 0 N = 0 since univ.erase 0 = ∅ in Fin 1. Tasaki’s formula −S(1 + zS) is intended for z ≥ 1 (γ-5 step 245) | Quantum/SpinS/SingleClusterHamiltonianCore.lean (PR #1292) |
| singleClusterHamiltonianS_allUp_expectation | All-up expectation: <Φ_⊤\|H\|Φ_⊤> = z·(N/2)² for the single-cluster Hamiltonian. Far above Tasaki’s GS energy −S(1+zS) since all-up is in the maximum-s_tot Casimir sector, not the minimum (γ-5 step 246) | Quantum/SpinS/SingleClusterHamiltonianCore.lean (PR #1293) |
| singleClusterHamiltonianS_allAligned_expectation | AllAligned-c expectation: <Φ_aligned(c)\|H\|Φ_aligned(c)> = z·(N/2 − c.val)². Generalises γ-5 step 246 (the c = 0 case). For c = Fin.last N (all-down) gives same z·(N/2)² (γ-5 step 247) | Quantum/SpinS/SingleClusterHamiltonianCore.lean (PR #1294) |
| singleClusterHamiltonianS_allDown_expectation | All-down expectation: <Φ_⊥\|H\|Φ_⊥> = z·(N/2)². Direct specialisation of γ-5 step 247 at c = Fin.last N (γ-5 step 248) | Quantum/SpinS/SingleClusterHamiltonianCore.lean (PR #1295) |
| leafSpinSOp{1,2,3} | Leaf-spin operators on Fin (z+1): Ŝ_R^(α) = Σ_{j ≠ 0} onSiteS j Ŝ^(α) for axes α = 1, 2, 3. Sum over leaves of single-site Ŝ^(α) (excludes central vertex 0). Building blocks for the upcoming Casimir decomposition H = (Ŝ_tot² − Ŝ_0² − Ŝ_R²)/2 (γ-5 step 249) | Quantum/SpinS/SingleClusterHamiltonianCore.lean (PR #1296) |
| singleClusterHamiltonianS_eq_dot_leaves | Ŝ_0 · Ŝ_R decomposition: H = Σ_α onSiteS 0 (Ŝ^(α)) · leafSpinSOp_α. Direct distribution of left multiplication over the sum Σ_j (A * B_j) = A * (Σ_j B_j) via Finset.mul_sum (γ-5 step 250) | Quantum/SpinS/SingleClusterHamiltonianCore.lean (PR #1297) |
| totalSpinSOp1/2/3_eq_onSite_zero_add_leafSpinSOp1/2/3 | Total = central + leaves (per axis): totalSpinSOp_α (Fin (z+1)) N = onSiteS 0 (Ŝ^(α)) + leafSpinSOp_α z N. Direct from Finset.sum_erase_add + add_comm (γ-5 step 251) | Quantum/SpinS/SingleClusterHamiltonianCore.lean (PR #1298) |
| leafSpinSSquared | Leaf-spin Casimir: Ŝ_R² := (Ŝ_R^(1))² + (Ŝ_R^(2))² + (Ŝ_R^(3))², total-spin-squared restricted to leaves of Fin (z+1) (γ-5 step 252) | Quantum/SpinS/SingleClusterHamiltonianCore.lean (PR #1299) |
| onSiteS_zero_commute_leafSpinSOp{1,2,3} | Center-leaf commutativity: Commute (onSiteS 0 Ŝ^(α)) (leafSpinSOp_α z N). Direct from Commute.sum_right + onSiteS_commute_of_ne (disjoint sites) (γ-5 step 253) | Quantum/SpinS/SingleClusterHamiltonianCore.lean (PR #1300) |
| singleClusterHamiltonianS_two_mul_eq_casimir_diff | Casimir decomposition: 2·H = (Ŝ_tot)² − Ŝ_0² − Ŝ_R² for the single-cluster Hamiltonian, where Ŝ_0² = spinSDot 0 0 N and Ŝ_R² = leafSpinSSquared z N. Proof: expand Σ_α totalSpinSOp_α² = Σ_α (onSite 0 + leaf_α)² via γ-5 step 251 + (a+b)² = a² + 2ab + b² (using γ-5 step 253 commutativity) + γ-5 step 250 (cross term identification) + noncomm_ring (γ-5 step 254) | Quantum/SpinS/SingleClusterHamiltonianCore.lean (PR #1301) |
| singleClusterHamiltonianS_two_smul_eq_casimir_diff | ℂ-smul Casimir form: (2 : ℂ) • H = (Ŝ_tot)² − Ŝ_0² − Ŝ_R². Direct corollary of γ-5 step 254 via two_mul + two_smul (γ-5 step 255) | Quantum/SpinS/SingleClusterHamiltonianCore.lean (PR #1302) |
| singleClusterHamiltonianS_two_mul_expectation | Casimir decomposition expectation form: 2 · <v\|H\|v> = <v\|Stot²\|v> − <v\|S0²\|v> − <v\|SR²\|v> for any v. Direct corollary of γ-5 step 255 + linearity of dotProduct + mulVec over smul and subtraction (γ-5 step 256) | Quantum/SpinS/SingleClusterHamiltonianCore.lean (PR #1303) |
| spinSDot_self_expectation_general | Single-site Casimir expectation: <v\|spinSDot x x N\|v> = (N(N+2)/4) · <v\|v> for any v. Direct from spinSDot_self (= scalar matrix) + linearity. Used to evaluate the S0² term in the Casimir decomposition (γ-5 step 257) | Quantum/SpinS/SingleClusterHamiltonianCore.lean (PR #1304) |
| singleClusterHamiltonianS_two_mul_expectation_simplified | Simplified Casimir expectation: 2 · <v\|H\|v> = <v\|Stot²\|v> − (N(N+2)/4)·<v\|v> − <v\|SR²\|v>. Combines γ-5 step 256 + 257; the S0² term is now an explicit scalar multiple of the norm-squared (γ-5 step 258) | Quantum/SpinS/SingleClusterHamiltonianCore.lean (PR #1305) |
| singleClusterHamiltonianS_eigenvalue_of_joint_casimir_eigenvec | H eigenvalue from joint Casimir eigenvalues: if Stot²·v = α·v and SR²·v = β·v, then H·v = (α − N(N+2)/4 − β)/2 · v. Reduces the GS-energy problem to enumerating admissible (α, β) joint eigenvalues (γ-5 step 259) | Quantum/SpinS/SingleClusterHamiltonian.lean (PR #1306) |
| spinSDot_self_mulVec_eq_smul | Single-site Casimir as scalar action: spinSDot x x N · v = (N(N+2)/4) • v for any v. Direct from spinSDot_self (= scalar matrix). Standalone helper extracted from γ-5 step 259 (γ-5 step 260) | Quantum/SpinS/SingleClusterHamiltonian.lean (PR #1307) |
| leafSpinSOp{1,2,3}_zero_z and leafSpinSSquared_zero_z | Edge case z=0 (single vertex, no leaves): leafSpinSOp_α 0 N = 0 and leafSpinSSquared 0 N = 0 since univ.erase 0 = ∅ in Fin 1 (γ-5 step 261) | Quantum/SpinS/SingleClusterHamiltonian.lean (PR #1308) |
| leafSpinSSquared_eq_sum_spinSDot | leafSpinSSquared as double sum: leafSpinSSquared z N = Σ_{j,k ∈ univ.erase 0} spinSDot j k N. Mirrors totalSpinSSquared_eq_sum_spinSDot for the leaf-only Casimir (γ-5 step 262) | Quantum/SpinS/SingleClusterHamiltonian.lean (PR #1309) |
| leafSpinSSquared_allUp_expectation | All-up expectation: <Φ_⊤\|leafSpinSSquared z N\|Φ_⊤> = (zN/2)·(zN/2 + 1) = s_R(s_R+1) where s_R = z·(N/2) is max leaf spin. Computed by rearranging γ-5 step 254 (Casimir decomposition) and applying closed forms for <Stot²>, <S0²>, <H> (γ-5 step 263) | Quantum/SpinS/SingleClusterHamiltonian.lean (PR #1310) |
| singleClusterHamiltonianS_mulVec_allAlignedStateS_zero | Eigenvector form on allUp: H · \|Φ_⊤⟩ = z·(N/2)² · \|Φ_⊤⟩. Proof: each leaf-pair spinSDot 0 j at j ≠ 0 gives (N²/4)·\|Φ_⊤⟩ (via spinSDot_mulVec_allAlignedStateS_zero_of_ne); sum over z leaves (γ-5 step 264) | Quantum/SpinS/SingleClusterHamiltonian.lean (PR #1311) |
| leafSpinSSquared_mulVec_allAlignedStateS_zero | Eigenvector form of Ŝ_R² on allUp: Ŝ_R² · \|Φ_⊤⟩ = (zN/2)·(zN/2+1) · \|Φ_⊤⟩. Witnesses that \|Φ_⊤⟩ is in the maximum-leaf-spin Casimir sector s_R = zN/2. Combined with γ-5 step 264 + existing Stot² eigenvector identity, confirms \|Φ_⊤⟩ is a joint eigenstate of H, Stot², Ŝ_0², Ŝ_R². Proof: rearrange γ-5 step 255 + apply (γ-5 step 265) | Quantum/SpinS/SingleClusterHamiltonian.lean (PR #1312) |
| singleClusterHamiltonianS_mulVec_allAlignedStateS_last | Eigenvector form on allDown: H · \|Φ_⊥⟩ = z·(N/2)² · \|Φ_⊥⟩. AllDown mirror of γ-5 step 264; same eigenvalue (spin-flip symmetry) (γ-5 step 266) | Quantum/SpinS/SingleClusterHamiltonian.lean (PR #1313) |
| leafSpinSSquared_mulVec_allAlignedStateS_last | Eigenvector form of Ŝ_R² on allDown: Ŝ_R² · \|Φ_⊥⟩ = (zN/2)·(zN/2+1) · \|Φ_⊥⟩. AllDown mirror of γ-5 step 265; both \|Φ_⊤⟩ and \|Φ_⊥⟩ lie in the maximum-leaf-spin Casimir sector s_R = zN/2, differing only by total Ŝ_tot^(3) magnetization (γ-5 step 267) | Quantum/SpinS/SingleClusterHamiltonian.lean (PR #1314) |
| singleClusterHamiltonianS_eigenvalue_at_gs_casimir_sector | GS-sector eigenvalue specialization: if v is a joint eigenvector of Ŝ_tot² at ((z−1)N/2)((z−1)N/2+1) and Ŝ_R² at (zN/2)(zN/2+1), then H · v = −(N/2)·(zN/2+1) · v = −S(1+zS) · v. Specialization of γ-5 step 259 to the ground-state sector predicted by Tasaki Problem 2.5.a (γ-5 step 268) | Quantum/SpinS/SingleClusterHamiltonian.lean (PR #1315) |
| singleClusterHamiltonianS_eigenvalue_at_max_casimir_sector | Max-Casimir-sector eigenvalue specialization: if v is a joint eigenvector of Ŝ_tot² at ((z+1)N/2)((z+1)N/2+1) and Ŝ_R² at (zN/2)(zN/2+1), then H · v = z·(N/2)² · v = zS² · v. Maximum Casimir sector containing \|Φ_⊤⟩, \|Φ_⊥⟩ (γ-5 step 269) | Quantum/SpinS/SingleClusterHamiltonian.lean (PR #1316) |
| singleClusterGSEnergyS / singleClusterHamiltonianS_mulVec_eq_gs_energy_smul | Predicted ground-state energy (Tasaki Problem 2.5.a target): singleClusterGSEnergyS z N := −(N/2)·(zN/2+1) = −S(1+zS), with named eigenvalue identity H · v = singleClusterGSEnergyS z N • v at the GS Casimir sector (γ-5 step 270) | Quantum/SpinS/SingleClusterHamiltonian.lean (PR #1317) |
| singleClusterMaxEnergyS / singleClusterHamiltonianS_mulVec_eq_max_energy_smul | Maximum Casimir-sector energy: singleClusterMaxEnergyS z N := z·(N/2)² = zS², with named eigenvalue identity H · v = singleClusterMaxEnergyS z N • v at the max Casimir sector containing \|Φ_⊤⟩, \|Φ_⊥⟩ (γ-5 step 271) | Quantum/SpinS/SingleClusterHamiltonian.lean (PR #1318) |
| singleClusterGSEnergyS_re_le_zero / singleClusterMaxEnergyS_re_nonneg | Energy real-part sign hygiene: Re(GS) ≤ 0 (AFM physical bound) and 0 ≤ Re(Max) (extremal aligned-state eigenvalue is non-negative) (γ-5 step 272) | Quantum/SpinS/SingleClusterHamiltonianEnergy.lean (PR #1319) |
| singleClusterGSEnergyS_re_le_singleClusterMaxEnergyS_re | Energy ordering: Re(GS) ≤ Re(Max). Consistency check between γ-5 steps 268 and 269 (γ-5 step 273) | Quantum/SpinS/SingleClusterHamiltonianEnergy.lean (PR #1320) |
| singleClusterGSEnergyS_im_zero / singleClusterMaxEnergyS_im_zero | Energies are real: imaginary parts of both named single-cluster energies vanish (γ-5 step 274) | Quantum/SpinS/SingleClusterHamiltonianEnergy.lean (PR #1321) |
| singleClusterGSEnergyS_one_eq / singleClusterMaxEnergyS_one_eq | Dimer (z=1) closed forms: singleClusterGSEnergyS 1 N = −(N/2)(N/2+1) = −S(S+1) (canonical singlet eigenvalue of Ŝ_0·Ŝ_1); singleClusterMaxEnergyS 1 N = (N/2)² = S² (canonical triplet eigenvalue) (γ-5 step 275) | Quantum/SpinS/SingleClusterHamiltonianEnergy.lean (PR #1322) |
| singleClusterGSEnergyS_zero_right / singleClusterMaxEnergyS_zero_right / singleClusterMaxEnergyS_zero_left | Trivial edge cases: GS z 0 = 0 (spin-0), Max z 0 = 0 (spin-0), Max 0 N = 0 (single-site, no leaves) (γ-5 step 276) | Quantum/SpinS/SingleClusterHamiltonianEnergy.lean (PR #1323) |
| singleClusterGSEnergyS_re_eq / singleClusterMaxEnergyS_re_eq | Explicit .re forms as ℝ values: Re(GS) = -(N/2)(zN/2+1), Re(Max) = z·N²/4. Useful for downstream real comparisons (γ-5 step 278) | Quantum/SpinS/SingleClusterHamiltonianEnergy.lean (PR #1325) |
| singleClusterMaxEnergyS_sub_singleClusterGSEnergyS | GS-Max energy gap: Max − GS = (N/2)(zN+1) = S(2zS+1). Closed-form difference between the two named eigenvalues (γ-5 step 280) | Quantum/SpinS/SingleClusterHamiltonianEnergy.lean (PR #1327) |
| singleClusterGSEnergyS_re_lt_singleClusterMaxEnergyS_re_of_pos | Strict gap for N ≥ 1: Re(GS) < Re(Max) whenever spin is non-trivial (γ-5 step 281) | Quantum/SpinS/SingleClusterHamiltonianEnergy.lean (PR #1328) |
| singleClusterGSEnergyS_re_neg_of_pos / singleClusterMaxEnergyS_re_pos_of_pos | Strict sign: Re(GS) < 0 for N ≥ 1; 0 < Re(Max) for z ≥ 1, N ≥ 1. Strengthens γ-5 step 272 (γ-5 step 283) | Quantum/SpinS/SingleClusterHamiltonianEnergy.lean (PR #1330) |
| leafSpinSSquared_one | Single-leaf reduction: leafSpinSSquared 1 N = spinSDot 1 1 N on Fin 2. Single-leaf leaf-Casimir collapses to single-site Casimir (γ-5 step 285) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1332) |
| leafSpinSSquared_one_mulVec / singleClusterHamiltonianS_eigenvalue_dimer | Dimer eigenvalue from Stot² alone: at z=1, leafSpinSSquared acts as the scalar N(N+2)/4, so any Stot² eigenvector is auto a joint eigenvector with H · v = ((α − N(N+2)/2) / 2) • v (γ-5 step 286) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1333) |
| singleClusterHamiltonianS_eigenvalue_dimer_singlet | Dimer singlet attains GS energy: for z=1, any Stot² = 0 eigenvector is an H-eigenvector at singleClusterGSEnergyS 1 N. Strongest concrete realisation of Tasaki Problem 2.5.a in the dimer case (γ-5 step 287) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1334) |
| singleClusterHamiltonianS_eigenvalue_dimer_top | Dimer top-spin attains Max energy: for z=1, any Stot² = N(N+1) eigenvector (s_tot = 2S) is an H-eigenvector at singleClusterMaxEnergyS 1 N (γ-5 step 288) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1335) |
| leafSpinSSquared_two | Trimer (z=2) leaf-Casimir decomposition: leafSpinSSquared 2 N = (N(N+2)/2) • 1 + 2 • spinSDot 1 2 N on Fin 3. Two diagonal spinSDot j j terms collapse to N(N+2)/4 • 1 each; off-diagonal spinSDot 1 2, spinSDot 2 1 are equal by spinSDot_comm (γ-5 step 292) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1339) |
| singleClusterHamiltonianS_eigenvalue_trimer | Trimer eigenvalue from Stot² + leaf-leaf coupling: for z=2, joint eigenvector of Stot² (=α) and spinSDot 1 2 (=β) is an H-eigenvector at (α − 3·N(N+2)/4 − 2β)/2. Specialisation of γ-5 step 259 using γ-5 step 292 (γ-5 step 293) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1340) |
| singleClusterHamiltonianS_eigenvalue_trimer_gs | Trimer GS-sector eigenvalue at GS energy: for z=2, joint eigenvector of Stot²·v=(N(N+2)/4)·v (s_tot=N/2) and spinSDot 1 2·v=(N²/4)·v (leaf triplet) is an H-eigenvector at singleClusterGSEnergyS 2 N = -N(N+1)/2 (γ-5 step 294) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1341) |
| singleClusterHamiltonianS_eigenvalue_trimer_top | Trimer top-spin sector eigenvalue at Max energy: for z=2, joint eigenvector at s_tot=3N/2 (max) and leaf triplet s_R=N is an H-eigenvector at singleClusterMaxEnergyS 2 N = N²/2 (γ-5 step 295) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1342) |
| singleClusterHamiltonianS_eigenvalue_trimer_leaf_singlet | Trimer leaf-singlet sector eigenvalue = 0: for z=2, joint eigenvector at s_tot=N/2 and leaf singlet s_R=0 (spinSDot 1 2·v = -(N(N+2)/4)·v) gives H · v = 0. Decoupling sector containing 0 from spin-1/2 trimer spectrum {-1, 0, 1/2} (γ-5 step 296) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1343) |
| leafSpinSSquared_three | Quartet (z=3) leaf-Casimir decomposition: leafSpinSSquared 3 N = (3·N(N+2)/4) • 1 + 2 • (spinSDot 1 2 + spinSDot 1 3 + spinSDot 2 3) on Fin 4. Three diagonal spinSDot j j terms collapse via spinSDot_self; six off-diagonal pair up via spinSDot_comm (γ-5 step 303) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1350) |
| singleClusterHamiltonianS_eigenvalue_quartet | Quartet eigenvalue from Stot² + leaf-leaf sum: for z=3, joint eigenvector of Stot² (=α) and (spinSDot 1 2 + spinSDot 1 3 + spinSDot 2 3) (=γ) is an H-eigenvector at (α − N(N+2) − 2γ)/2. Specialisation of γ-5 step 259 using γ-5 step 303 (γ-5 step 304) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1351) |
| singleClusterHamiltonianS_eigenvalue_quartet_gs | Quartet GS-sector at GS energy: for z=3, joint eigenvector at Stot²·v=N(N+1)·v (s_tot=N) and leaf-leaf sum (3N²/4)·v (max leaf-spin s_R=3N/2) gives H · v = singleClusterGSEnergyS 3 N · v = -N(3N+2)/4 · v (γ-5 step 305) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1352) |
| singleClusterHamiltonianS_eigenvalue_quartet_top | Quartet top-spin sector at Max energy: for z=3, joint eigenvector at Stot²·v=2N(2N+1)·v (s_tot=2N=(z+1)N/2) and leaf-leaf sum (3N²/4)·v (max leaf-spin s_R=3N/2) gives H · v = singleClusterMaxEnergyS 3 N · v = 3N²/4 · v (γ-5 step 306) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1353) |
← Total spin operator (Tasaki §2.2 eq. (2.2.7), (2.2.8)) · Catalogue · Total spin operator (Tasaki §2.2 eq. (2.2.7), (2.2.8)) →