S saturated ferromagnetic state (Tasaki §2.4 generalised) (part 1 of 2)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 saturated ferromagnetic state (Tasaki §2.4 generalised)Pruned rows (PR #5143, issue #5140). 25 rows of the ladder-iterate route were removed from this section; see Deleted routes for what they documented.
Generic-spin (N = 2S) version of Tasaki §2.4 P1i for the
saturated ferromagnet: the all-aligned (constant-spin) basis
state |σ_⊤⟩ = ⊗_x |c⟩ with σ x = c for all x : V. The two
extremal weights c = 0 (highest weight, “all up”) and
c = Fin.last N (lowest weight, “all down”) are the highest- and
lowest-weight vectors of the J_tot = |V|·S = |V|·N/2 irreducible
SU(2) representation in the multi-site Hilbert space. Tracked in
Issue #412; assembled in PRs #875–#879. The foundational all-aligned theorems live in
Quantum/SpinS/AllAlignedStateCore.lean (the ladder-preservation results remain in Quantum/SpinS/AllAlignedState.lean).
| Lean name | Statement |
|—|—|
| allAlignedConfigS V N c | constant configuration σ x = c (PR #875) |
| allAlignedStateS V N c | basis state at constant c, equal to basisVecS (allAlignedConfigS V N c) (PR #875) |
| magSumS_allAlignedConfigS | magSumS = |V|·c.val (PR #875) |
| magEigenvalueS_allAlignedConfigS | magEigenvalueS = |V|·N/2 − |V|·c (PR #875) |
| totalSpinSOp3_mulVec_allAlignedStateS | Ŝ^z_tot · |c⟩ = (|V|·N/2 − |V|·c) · |c⟩ for any c (PR #875) |
| magSumS_allAlignedConfigS_zero | c = 0 ⟹ magSumS = 0 (PR #875) |
| magSumS_pos_of_ne_allAlignedConfigS_zero | the all-up configuration is the unique magSumS = 0 configuration (PR #875) |
| magSumS_allAlignedConfigS_last | c = Fin.last N ⟹ magSumS = |V|·N (PR #876) |
| magSumS_lt_card_mul_of_ne_allAlignedConfigS_last | the all-down configuration is the unique configuration with magSumS = |V|·N (PR #876) |
| heisenbergHamiltonianS_mulVec_allAlignedStateS_zero | the all-up state is a Heisenberg eigenvector for ANY coupling — magnetization conservation [H, Ŝ^z_tot] = 0 + uniqueness of the M=0 configuration (PR #875) |
| heisenbergHamiltonianS_mulVec_allAlignedStateS_zero_eigenvalue | explicit Heisenberg eigenvalue formula on all-up: Σ_x J(x,x)·N(N+2)/4 + Σ_{x≠y} J(x,y)·N²/4 (PR #875) |
| heisenbergHamiltonianS_mulVec_allAlignedStateS_last / _eigenvalue | symmetric c = N (all-down) Heisenberg eigenvector + same eigenvalue formula (PR #876) |
| onSiteS_spinSOpPlus_apply_allAlignedConfigS_zero | (onSiteS x Ŝ^+) σ' σ_⊤ = 0 (PR #877) |
| onSiteS_spinSOpPlus_mulVec_allAlignedStateS_zero | (onSiteS x Ŝ^+).mulVec |σ_⊤⟩ = 0 (PR #877) |
| totalSpinSOpPlus_mulVec_allAlignedStateS_zero | Ŝ^+_tot · |σ_⊤⟩ = 0 (highest-weight annihilation, PR #877) |
| onSiteS_spinSOpMinus_apply_allAlignedConfigS_last / onSiteS_spinSOpMinus_mulVec_allAlignedStateS_last / totalSpinSOpMinus_mulVec_allAlignedStateS_last | symmetric lowest-weight annihilation Ŝ^-_tot · |σ_⊥⟩ = 0 (PR #877) |
| totalSpinSSquared_mulVec_allAlignedStateS_zero | the all-up state is a (Ŝ_tot)²-eigenvector (PR #878) |
| totalSpinSSquared_apply_diag_allAlignedConfigS_zero | explicit Casimir diagonal value |V|·N(N+2)/4 + (|V|²−|V|)·N²/4 (PR #878) |
| totalSpinSSquared_mulVec_allAlignedStateS_zero_eigenvalue | (Ŝ_tot)² · |σ_⊤⟩ = (|V|·N/2)·(|V|·N/2 + 1) · |σ_⊤⟩ — operator-level form of “all-up is the highest-weight vector of the J_tot = |V|·S irreducible SU(2) representation” (PR #878) |
| totalSpinSSquared_mulVec_allAlignedStateS_last / totalSpinSSquared_apply_diag_allAlignedConfigS_last / _eigenvalue | symmetric lowest-weight Casimir eigenvalue (same value) (PR #879) |
| heisenbergHamiltonianS_commute_totalSpinSOp1 / _Op2 / _OpPlus / _OpMinus | Commute-form conversions: H commutes with each axis-total operator (PR #881) |
| heisenbergHamiltonianS_commute_totalSpinSOpMinus_pow / _Plus_pow | iterated power Commute by induction (PR #881) |
| heisenbergHamiltonianS_mulVec_totalSpinSOpMinus_pow_allAlignedStateS_zero | for any k, (Ŝ^-_tot)^k · |σ_⊤⟩ is a Heisenberg eigenvector at the same eigenvalue as |σ_⊤⟩ (PR #881) |
| heisenbergHamiltonianS_mulVec_totalSpinSOpPlus_pow_allAlignedStateS_last | symmetric for Ŝ^+_tot on all-down (PR #881) |
| totalSpinSSquared_commute_totalSpinSOp1 / _Op2 / _OpPlus / _OpMinus / _OpMinus_pow / _OpPlus_pow | Casimir Commute-form analogues (PR #882) |
| totalSpinSSquared_mulVec_totalSpinSOpMinus_pow_allAlignedStateS_zero | for any k, (Ŝ^-_tot)^k · |σ_⊤⟩ preserves the Casimir eigenvalue (|V|·N/2)·(|V|·N/2+1) (PR #882) |
| totalSpinSSquared_mulVec_totalSpinSOpPlus_pow_allAlignedStateS_last | symmetric (PR #882) |
| totalSpinSOp3_commutator_totalSpinSOpMinus | multi-site Cartan: [Ŝ^z_tot, Ŝ^-_tot] = -Ŝ^-_tot (PR #883) |
| totalSpinSOp3_commutator_totalSpinSOpPlus | multi-site Cartan: [Ŝ^z_tot, Ŝ^+_tot] = +Ŝ^+_tot (PR #883) |
| totalSpinSOp3_mulVec_totalSpinSOpMinus_mulVec_allAlignedStateS_zero | single-step magnetic-quantum-number shift: Ŝ^z_tot · (Ŝ^-_tot · |σ_⊤⟩) = (|V|·N/2 − 1) · (Ŝ^-_tot · |σ_⊤⟩) — the once-lowered all-up state is an Ŝ^z_tot eigenvector with magnetic quantum number m_max − 1 (PR #886) |
| totalSpinSOp3_mulVec_totalSpinSOpPlus_mulVec_allAlignedStateS_last | symmetric: Ŝ^z_tot · (Ŝ^+_tot · |σ_⊥⟩) = (−|V|·N/2 + 1) · (Ŝ^+_tot · |σ_⊥⟩) (PR #886) |
| totalSpinSOp3_mulVec_totalSpinSOpMinus_mulVec_eigenvec / _OpPlus_mulVec_eigenvec | generic single-step shift on any Ŝ^z_tot eigenvector: Ŝ^z_tot ψ = λ ψ ⇒ Ŝ^z_tot (Ŝ^∓_tot ψ) = (λ ∓ 1) (Ŝ^∓_tot ψ). Proven via the multi-site Cartan rearrangement Ŝ^z_tot · Ŝ^∓_tot = Ŝ^∓_tot · Ŝ^z_tot ∓ Ŝ^∓_tot lifted to mulVec (PR #887) |
| totalSpinSOp3_mulVec_totalSpinSOpMinus_pow_allAlignedStateS_zero | iterated magnetic-quantum-number labelling Ŝ^z_tot · ((Ŝ^-_tot)^k · |σ_⊤⟩) = (|V|·N/2 − k) · ((Ŝ^-_tot)^k · |σ_⊤⟩) for every k : ℕ. Inducts at the eigenvector level using the generic single-step shift _eigenvec, bypassing the technically delicate operator-level iterated Cartan (PR #887) |
| totalSpinSOp3_mulVec_totalSpinSOpPlus_pow_allAlignedStateS_last | symmetric for (Ŝ^+_tot)^k · |σ_⊥⟩ with eigenvalue −|V|·N/2 + k (PR #887) |
| magSubspaceS_eq_eigenspace / magSubspaceS_iSupIndep / magSubspaceS_isInternal | spin-S magnetization subspaces form an internal direct sum decomposition: bridge to Module.End.eigenspace, distinct-eigenvalue independence (via Module.End.eigenspaces_iSupIndep over ℂ), combined with the existing iSup_magSubspaceS_eq_top (PR #889, file Quantum/SpinS/MagnetizationDirectSum.lean) |
| totalSpinSOpMinus_pow_allAlignedStateS_zero_mem_magSubspaceS / totalSpinSOpPlus_pow_allAlignedStateS_last_mem_magSubspaceS | PR #887 ladder iterates lie in the magnetization sectors magSubspaceS V N (m_max ∓ k) (PR #889 corollaries) |
| oneFlippedUpConfig V x_0 hN / oneFlippedDownConfig V x_0 hN | one-flipped configurations: 0 → 1 at site x_0 (resp. N → N-1), all other sites at 0 (resp. N); requires 0 < N (PR #890, file Quantum/SpinS/LadderIterateNonvanishing.lean) |
| totalSpinSOpMinus_mulVec_allAlignedStateS_zero_at_oneFlippedUpConfig | explicit value ((Ŝ^-_tot · |σ_⊤⟩)) (oneFlippedUpConfig V x_0) = √N. Proof distributes via Matrix.sum_mulVec, isolates only the pivot site x_0, reduces via spinSOpMinus_apply_lower N (0 + 1 = 1) = √(N · 1) (PR #890) |
| totalSpinSOpMinus_mulVec_allAlignedStateS_zero_ne_zero | for 0 < N and [Nonempty V], Ŝ^-_tot · |σ_⊤⟩ ≠ 0. Witness: value at oneFlippedUpConfig is √N > 0 (PR #890) |
| totalSpinSOpPlus_mulVec_allAlignedStateS_last_at_oneFlippedDownConfig / totalSpinSOpPlus_mulVec_allAlignedStateS_last_ne_zero | symmetric for the raising side Ŝ^+_tot · |σ_⊥⟩ (PR #890) |
| allAlignedStateS_ne_zero | the all-aligned state at any constant c : Fin (N+1) is non-zero (its value at the all-aligned config is 1) (PR #891, file Quantum/SpinS/SaturatedPairLinearIndependent.lean) |
| allAlignedStateS_zero_mem_eigenspace_mMax / allAlignedStateS_last_mem_eigenspace_negMMax | the all-up / all-down state lies in Module.End.eigenspace of (Ŝ^z_tot).mulVecLin at ±m_max = ±|V|·N/2 (PR #891) |
| totalSpinSOpMinus_mulVec_allAlignedStateS_zero_mem_eigenspace_mMaxSubOne / totalSpinSOpPlus_mulVec_allAlignedStateS_last_mem_eigenspace_negMMaxAddOne | the once-lowered (resp. raised) state lies in Module.End.eigenspace at m_max − 1 (resp. −m_max + 1) (PR #891) |
| allAlignedStateS_zero_totalSpinSOpMinus_mulVec_linearIndependent / allAlignedStateS_last_totalSpinSOpPlus_mulVec_linearIndependent | {|σ_⊤⟩, Ŝ^-_tot · |σ_⊤⟩} is LinearIndependent ℂ for 0 < N and [Nonempty V] (and the symmetric raising version). Combines #875, #886, #889, #890 via Module.End.eigenvectors_linearIndependent' with the eigenvalue pair (m_max, m_max − 1) (PR #891) |
| totalSpinSOpPlus_commutator_totalSpinSOpMinus / totalSpinSOpMinus_commutator_totalSpinSOpPlus | multi-site Cartan ⁺⁻: [Ŝ^+_tot, Ŝ^-_tot] = 2 · Ŝ^z_tot (and antisymmetric −2 · Ŝ^z_tot); lifts the single-site spinSOpPlus_commutator_spinSOpMinus via onSiteS_commutator_totalOnSiteS (PR #893, file Quantum/SpinS/MultiSiteCartanPlusMinus.lean) |
| totalSpinSOpPlus_mul_totalSpinSOpMinus_add_totalSpinSOpMinus_mul_totalSpinSOpPlus | sum identity Ŝ^+_tot · Ŝ^-_tot + Ŝ^-_tot · Ŝ^+_tot = 2 · ((Ŝ^{(1)}_tot)² + (Ŝ^{(2)}_tot)²); the ±i [A, B] cross terms cancel in the sum of (A ± iB)(A ∓ iB) (PR #894, file Quantum/SpinS/CasimirRearrangement.lean) |
| totalSpinSOpPlus_mul_totalSpinSOpMinus_eq_casimir_minus_z_sq_add_z / totalSpinSOpMinus_mul_totalSpinSOpPlus_eq_casimir_minus_z_sq_sub_z | Casimir rearrangement: Ŝ^+_tot · Ŝ^-_tot = Ŝ_tot² − (Ŝ^z_tot)² + Ŝ^z_tot (and symmetric − Ŝ^z_tot for MinusPlus). Combines the sum identity with the Cartan ⁺⁻ (#893), then uses totalSpinSSquared_def (PR #894) |
| totalSpinSOpPlus_mulVec_totalSpinSOpMinus_pow_succ_allAlignedStateS_zero | the eigenvalue identity Ŝ^+_tot · ((Ŝ^-_tot)^(k+1) · |σ_⊤⟩) = (k+1)(|V|·N − k) · ((Ŝ^-_tot)^k · |σ_⊤⟩), derived from the Casimir rearrangement (#894) + iterate eigenvalue identities (#882, #887) (PR #895, file Quantum/SpinS/IterateInductiveNonvanishing.lean) |
| totalSpinSOpMinus_pow_allAlignedStateS_zero_ne_zero | inductive non-vanishing: for [Nonempty V] and k ≤ |V|·N, the iterate (Ŝ^-_tot)^k · |σ_⊤⟩ is non-zero. Inductive proof via the eigenvalue identity above (PR #895) |
| ladderIterateUp V N k / ladderEigenvalueUp V N k / ladderEigenvalueUp_injective / ladderIterateUp_mem_eigenspace / ladderIterateUp_hasEigenvector | the (2m_max + 1)-element ladder family parameterised by Fin (|V|·N + 1), its Ŝ^z_tot-eigenvalue function m_max − k, the injectivity of the eigenvalue function, and the per-k Module.End.HasEigenvector witnesses (PR #896, file Quantum/SpinS/SaturatedFullLadderLI.lean) |
| ladderIterateUp_linearIndependent | 🎯 full saturated-ferromagnet ladder LI: for [Nonempty V], the family {(Ŝ^-_tot)^k · |σ_⊤⟩ : k ∈ Fin (|V|·N + 1)} of 2m_max + 1 iterates is LinearIndependent ℂ. Applies Module.End.eigenvectors_linearIndependent' to the per-k HasEigenvector witnesses with the injective m_max − k eigenvalue function. The Tasaki §2.4 saturated-ferromagnet ground-state ladder basis identification (PR #896) |
| Matrix.IsHermitian.dotProduct_eq_zero_of_eigenvalues_ne (generic) | for a Hermitian matrix M : Matrix n n ℂ, two eigenvectors at distinct real eigenvalues are orthogonal in dotProduct (star v) w. Proof: α · ⟨v,w⟩ = ⟨Mv,w⟩ = ⟨v,Mw⟩ = β · ⟨v,w⟩, using Matrix.star_mulVec and Hermiticity (PR #898, file Quantum/SpinS/SaturatedFullLadderOrthogonality.lean) |
| ladderEigenvalueUp_star_eq / ladderIterateUp_orthogonal | the ladder eigenvalues are real (star = self); pairwise orthogonality of the saturated-ferromagnet ladder iterates: for [Nonempty V] and i ≠ j, dotProduct (star (ladderIterateUp V N i)) (ladderIterateUp V N j) = 0. The ladder iterates form an orthogonal basis (PR #898) |
| saturatedFerromagnetEigenvalueS J N / ladderIterateUp_mem_heisenbergHamiltonianS_eigenspace / ladderIterateUp_heisenbergHamiltonianS_hasEigenvector | the H-eigenvalue at the all-up configuration; each ladder iterate lies in the H-eigenspace at this eigenvalue; bundled Module.End.HasEigenvector (PR #899, file Quantum/SpinS/SaturatedLadderHEigenspace.lean) |
| heisenbergHamiltonianS_eigenspace_finrank_ge_succ_card_mul_N | H-eigenspace dimension lower bound: for [Nonempty V], the heisenbergHamiltonianS J N-eigenspace at the saturated-ferromagnet eigenvalue has Module.finrank ℂ ≥ |V|·N + 1 = 2m_max + 1. Restricts the LI family (#896) to the eigenspace via subtype embedding, applies LinearIndependent.fintype_card_le_finrank (PR #899) |
| saturatedFerromagnetCasimirEigenvalueS V N / ladderIterateUp_mem_totalSpinSSquared_eigenspace / ladderIterateUp_totalSpinSSquared_hasEigenvector / totalSpinSSquared_eigenspace_finrank_ge_succ_card_mul_N | mirror of #899 for the Casimir operator (Ŝ_tot)²: eigenvalue m_max(m_max + 1), eigenspace membership, HasEigenvector bundle, and finrank ≥ 2m_max + 1 lower bound (PR #900, file Quantum/SpinS/SaturatedLadderCasimirEigenspace.lean) |
| saturatedFerromagnetJointEigenspace J N / ladderIterateUp_mem_saturatedFerromagnetJointEigenspace / saturatedFerromagnetJointEigenspace_finrank_ge_succ_card_mul_N | the joint (H, (Ŝ_tot)²)-eigenspace at (c_J, m_max(m_max+1)) defined as the meet of the two individual eigenspaces; ladder iterate membership; finrank ≥ |V|·N + 1 = 2m_max + 1 (PR #903, file Quantum/SpinS/SaturatedLadderJointEigenspaceCore.lean) |
| magSubspaceS_mMax_inf_saturatedFerromagnetJointEigenspace / magSubspaceS_neg_mMax_inf_saturatedFerromagnetJointEigenspace | extremal magnetisation sectors ∩ joint eigenspace are 1-dimensional: H_{±m_max} ⊓ saturatedFerromagnetJointEigenspace J N = Submodule.span ℂ {|σ_⊤/⊥⟩}. First two concrete sector contributions toward the upper bound finrank(joint) ≤ 2m_max+1 that closes Tasaki §2.4 Theorem 2.1. Combines magSubspaceS_(±m_max)_eq_span_allAlignedStateS_(zero/last) (PR #908) with joint-eigenspace membership of |σ_⊤⟩ = ladderIterateUp V N 0 (resp. |σ_⊥⟩ via saturatedFerromagnetEigenvalueS_explicit and the _last_eigenvalue lemma) (PR #2759) |
| mulVec_preserves_eigenvalue_of_commuteS / totalSpinSOpPlus_mulVec_mem_saturatedFerromagnetJointEigenspace_inf_magSubspaceS | Ŝ^+_tot maps joint ⊓ H_M into joint ⊓ H_{M+1}: spin-S analogue of the generic eigenvalue propagation lemma plus its application to show the raising operator preserves joint-eigenspace membership while shifting the magnetisation by +1. Inductive step (toward proving the joint eigenspace decomposes as a chain of 1-dim sectors via injectivity of Ŝ^+_tot away from the highest-weight; key ingredient for the upper bound finrank(joint) ≤ 2m_max+1) (PR #2760) |
| totSpinSOpPlus_mulVecZero_imp_eq_zero_of_mem_satFerroJE_inf_magSubS | Ŝ^+_tot is injective on joint ⊓ H_M away from the highest-weight sector: for v ∈ joint ⊓ H_M with M ≠ m_max, if Ŝ^+_tot · v = 0 then v = 0. Proof via the MinusPlus Casimir rearrangement (PR #894): Ŝ^-_tot · Ŝ^+_tot = Ŝ_tot² − (Ŝ^z_tot)² − Ŝ^z_tot, so Ŝ^+_tot v = 0 implies (m_max − M)(m_max + M + 1) v = 0. The M = -m_max - 1 case is ruled out by PR #905’s magSubspaceS = ⊥ and M ≠ m_max is the hypothesis. Combined with the joint-magnetisation shift (PR #2760), gives the kernel-trivial inductive step toward Tasaki §2.4 Theorem 2.1 (PR #2761) |
| totalSpinSOpPlusJointMagShift / totalSpinSOpPlusJointMagShift_injective / saturatedFerromagnetJointEigenspace_inf_magSubspaceS_finrank_le_succ | Ŝ^+_tot as a linear map (joint ⊓ H_M) →ₗ[ℂ] (joint ⊓ H_{M+1}), its injectivity for M ≠ m_max, and the finrank chain dim(joint ⊓ H_M) ≤ dim(joint ⊓ H_{M+1}): packages PR #2760 (joint-magnetisation shift) and PR #2761 (kernel-trivial) into a single linear map and applies mathlib’s LinearMap.finrank_le_finrank_of_injective. PR #2763 iterates this chain to propagate the 1-dim bound at H_{m_max} (PR #2759) down to every sector; PR #2768 completes the final summation step via magProjFn to give joint = span(ladderIterateUp) and hence Tasaki §2.4 Theorem 2.1 (PR #2762) |
| saturatedFerromagnetJointEigenspace_inf_magSubspaceS_finrank_le_one | per-sector finrank ≤ 1: for every k : ℕ, Module.finrank ℂ (joint ⊓ H_{m_max − k}) ≤ 1. Proof by Nat induction on k: base case k = 0 uses PR #2759’s joint ⊓ H_{m_max} = span {|σ_⊤⟩} and finrank_span_singleton; step case uses the finrank chain (PR #2762). The 2m_max + 1 spectrum values M = m_max − k for k ∈ {0, ..., 2m_max} were combined in PR #2768 via the pointwise magnetisation decomposition to give joint = span(ladderIterateUp), completing Tasaki §2.4 Theorem 2.1 (PR #2763) |
| saturatedFerromagnetJointEigenspace_inf_magSubspaceS_eq_span_ladderIterateUp | per-sector identification = span (ladderIterateUp k): for every k : Fin (Fintype.card V * N + 1), joint ⊓ H_{m_max - k} = Submodule.span ℂ {ladderIterateUp V N k}. Combines per-sector ≤ 1-dim (PR #2763) with ladderIterateUp V N k ∈ joint (PR #903), ladderIterateUp V N k ∈ H_{m_max-k} (PR #889 via PR #887), and ladderIterateUp V N k ≠ 0 (PR #895). Apply Submodule.eq_of_le_of_finrank_le. Identifies each ladder iterate as the unique (up to scaling) non-zero vector in its joint-magnetisation sector. Summed across the 2m_max + 1 spectrum values in PR #2768 via the pointwise magnetisation decomposition to give joint = span(ladderIterateUp) (PR #2764) |
| magProjFn / magProjFn_mem_magSubspaceS | pointwise magnetisation projector: magProjFn M v σ is v σ if magEigenvalueS σ = M and 0 otherwise; lands in magSubspaceS V N M. First framework step toward decomposing joint eigenspace elements into per-sector components for the final Tasaki §2.4 Theorem 2.1 closure (PR #2765) |
| magSubspaceS_apply_eq_zero_of_magEigenvalueS_ne / magProjFn_add / magProjFn_smul / matrix_entry_eq_zero_of_mulVec_basisVecS_mem_magSubspaceS / heisenbergHamiltonianS_mulVec_magProjFn_eq | magProjFn linearity + commutation with H: support property of magSubspaceS V N M (vanishes off the magnetisation level), linearity of magProjFn in the vector argument, off-magnetisation matrix-entry vanishing for any magnetisation-preserving operator, and the Heisenberg commutation H · magProjFn M v = magProjFn M (H · v) via the matrix-entry vanishing applied to H · basisVecS τ (PR #1078) (PR #2766) |
| totalSpinSSquared_mulVec_magProjFn_eq / magProjFn_mem_saturatedFerromagnetJointEigenspace | Casimir commutation + joint preservation for magProjFn: (Ŝ_tot)² · magProjFn M v = magProjFn M ((Ŝ_tot)² · v) (same matrix-entry-vanishing argument as PR #2766, applied to (Ŝ_tot)² · basisVecS τ via PR #1078), and the joint preservation magProjFn M v ∈ joint for v ∈ joint combining the two commutations with magProjFn_smul (PR #2767) |
| sum_magProjFn_eq / saturatedFerromagnetJointEigenspace_le_span_ladderIterateUp / saturatedFerromagnetJointEigenspace_eq_span_ladderIterateUp | 🎯 Tasaki §2.4 Theorem 2.1 closure: joint = span (Set.range (ladderIterateUp V N)). (1) Pointwise decomposition v = Σ_{k} magProjFn (m_max - k.val) v (each σ has unique magSumS σ ∈ {0, ..., |V|N} selecting one term). (2) joint ⊆ span(ladderIterateUp): for v ∈ joint, each magnetisation component is in joint ⊓ H_{m_max - k.val} = span {ladderIterateUp V N k} (PR #2764 + PR #2767). (3) Combined with reverse inclusion span ⊆ joint (PR #904) via le_antisymm. Identifies the saturated-ferromagnet joint eigenspace as exactly the (2m_max + 1)-dim irreducible SU(2) representation generated by the lowering operator from |σ_⊤⟩ (PR #2768) |
| saturatedFerromagnetJointEigenspace_finrank_eq | operator-level dimension formula: Module.finrank ℂ (saturatedFerromagnetJointEigenspace J N) = |V|·N + 1 = 2m_max + 1. Direct corollary of the Theorem 2.1 closure (PR #2768): the joint eigenspace equals the linear span of the ladder iterates (PR #2768), whose finrank is |V|·N + 1 (PR #904). Promotes the lower bound finrank ≥ |V|·N + 1 (PR #903) to an equality at the operator level, identifying the saturated-ferromagnet joint eigenspace as the unique (2m_max + 1)-dimensional irreducible SU(2) representation (PR #2769) |
| magSubspaceS_eq_bot_of_not_in_spectrum / magEigenvalueS_ne_neg_mMax_sub_one / totalSpinSOpMinus_pow_succ_card_mul_N_allAlignedStateS_zero | for M : ℂ not in the spectrum of Ŝ^z_tot, magSubspaceS V N M = ⊥; −m_max − 1 is outside the spectrum; boundary annihilation (Ŝ^-_tot)^(|V|·N + 1) · |σ_⊤⟩ = 0 (PR #905, file Quantum/SpinS/LadderBoundaryAnnihilation.lean). Caps the saturated-ferromagnet ladder at exactly 2m_max + 1 non-zero terms |
| magEigenvalueS_ne_mMax_add_one / totalSpinSOpPlus_pow_succ_card_mul_N_allAlignedStateS_last | symmetric raising-side boundary annihilation (Ŝ^+_tot)^(|V|·N + 1) · |σ_⊥⟩ = 0 via m_max + 1 off-spectrum (PR #907, extends Quantum/SpinS/LadderBoundaryAnnihilation.lean) |
| magEigenvalueS_eq_mMax_iff_allAlignedConfigS_zero / magEigenvalueS_eq_neg_mMax_iff_allAlignedConfigS_last | the extremal eigenvalues ±m_max are achieved by exactly one configuration each (the all-up / all-down constant). Lifts PR #885’s magConfigS_card = 1 to magEigenvalueS = ±m_max characterisation (PR #908, file Quantum/SpinS/MagSubspaceExtremalDimCore.lean; the extremal-eigenvalue magnetization-subspace dimension stays in Quantum/SpinS/MagSubspaceExtremalDim.lean, split for build speed) |
| magSubspaceS_mMax_eq_span_allAlignedStateS_zero / magSubspaceS_neg_mMax_eq_span_allAlignedStateS_last | the extremal magnetization subspaces are 1-dimensional: magSubspaceS V N (±m_max) = Submodule.span ℂ {|σ_⊤/⊥⟩}. Analytic counterpart of #885 (PR #908) |
| basisVecS_inner_self / allAlignedStateS_inner_self / allAlignedStateS_{zero,last}_expectation_totalSpinSOp3 / allAlignedStateS_{zero,last}_expectation_totalSpinSSquared | expectation values on all-aligned states: norm-squared 1; Ŝ^z_tot expectation ±m_max; Casimir expectation m_max(m_max + 1) (PR #913, file Quantum/SpinS/AllAlignedStateExpectations.lean) |
| basisVecS_inner_of_ne / basisVecS_inner_kronecker / allAlignedStateS_zero_inner_allAlignedStateS_last | basisVecS orthonormality: distinct configs orthogonal; bundled Kronecker form; extremal all-aligned states orthogonal for [Nonempty V] and 0 < N (PR #914, file Quantum/SpinS/BasisVecSOrthonormal.lean) |
| spinSDot_self_mulVec / _expectation / _expectation_normalized / _expectation_allAlignedStateS | universal single-site Casimir expectation ⟨Φ, Ŝ_x · Ŝ_x · Φ⟩ = S(S+1) for normalized Φ. Direct from spinSDot_self. Foundation for Tasaki Problem 2.5.c (γ-7) (PR #920, file Quantum/SpinS/SingleSiteCasimirExpectation.lean) |
| singleSiteSpinSquareExpectationS / _axis_sum / _axis_sum_normalized / _axis1_eq_of_axes_equal_normalized / _all_axes_eq_of_axes_equal_normalized | Problem 2.5.c single-site squared-expectation bridge: packages ⟨Φ,(Ŝ_x^(α))² Φ⟩, proves the three-axis sum is the universal single-site Casimir expectation, and under normalized-state plus equal-axis hypotheses returns N(N+2)/12 = S(S+1)/3 for each Cartesian axis. This isolates the algebraic reduction while leaving the AFM ground-state SU(2)-symmetry input explicit. Tasaki, Springer 2020, Problem 2.5.c, p. 43 (PR #4056, file Quantum/SpinS/Problem25cSingleSiteSquared.lean) |
| dotProduct_star_mulVec_eq_dotProduct_star_conjTranspose_mulVec / singleSiteSpinSquareExpectationS_eq_of_conj_invariant | Problem 2.5.c unitary symmetry input: if a many-body unitary T conjugates a single-site spin component A to B, T† = T⁻¹, and the state is fixed by T⁻¹, then the squared single-site expectations of A and B are equal. This turns future SU(2)/axis-swap ground-state invariance into the equal-axis hypothesis required by PR #4056. Tasaki, Springer 2020, Problem 2.5.c, p. 43 and Theorem 2.4 context, pp. 43-44 (PR #4057, file Quantum/SpinS/Problem25cUnitaryAxisInput.lean) |
| manyBodyTensorS_conjTranspose / AxisSwapUnitaryS.tensor_conjTranspose / axisSwapUnitarySSpinS_tensor_conjTranspose / singleSiteSpinSquareExpectationS_axis3_eq_axis2_of_axisSwapInvariant | Problem 2.5.c lifted axis-swap adjoint input: proves (⊗_x W_x)† = ⊗_x W_x†, specializes U† = U⁻¹ to the many-body spin-S axis-swap tensor, and uses the PR #4057 bridge plus AxisSwapUnitaryS.tensor_conj_onSiteS to equate the axis-3 and axis-2 squared single-site expectations under an explicit lifted-axis-swap invariance hypothesis. Tasaki, Springer 2020, Problem 2.5.c, p. 43 and Theorem 2.4 context, pp. 43-44 (PR #4058, file Quantum/SpinS/Problem25cAxisSwapAdjointInput.lean) |
| singleSiteSpinSquareExpectationS_all_axes_eq_of_axisSwapInvariant_axis1_eq_axis2 | Problem 2.5.c axis-swap equal-axes wrapper: combines PR #4058’s axis-swap equality E_3 = E_2 with PR #4056’s all-axis algebraic bridge. For a normalized state fixed by the inverse lifted axis swap, one remaining explicit equality E_1 = E_2 implies E_1 = E_2 = E_3 = N(N+2)/12. This leaves the missing axis-1/axis-2 SU(2) or rotation input explicit. Tasaki, Springer 2020, Problem 2.5.c, p. 43 and Theorem 2.4 context, pp. 43-44 (PR #4059, file Quantum/SpinS/Problem25cAxisSwapEqualAxes.lean) |
| singleSiteSpinSquareExpectationS_axis1_eq_axis2_of_unitaryInvariant / _all_axes_eq_of_axisSwapInvariant_unitary_axis12 | Problem 2.5.c two-symmetry axis input: derives the remaining equality E_1 = E_2 from an explicit abstract unitary conjugation T Ŝ_x^(2) T⁻¹ = Ŝ_x^(1) plus T⁻¹Φ = Φ, then combines it with PR #4059’s lifted-axis-swap wrapper to conclude E_1 = E_2 = E_3 = N(N+2)/12. The concrete general spin-S rotation or AFM ground-state SU(2) invariance theorem remains explicit. Tasaki, Springer 2020, Problem 2.5.c, p. 43 and Theorem 2.4 context, pp. 43-44 (PR #4060, file Quantum/SpinS/Problem25cTwoSymmetryAxisInput.lean) |
| spinSRot3 / spinSRot3_neg_pi_half_conj_spinSOp2 / manyBodySpinSRot3_neg_pi_half_conj_onSiteS_spinSOp2 / singleSiteSpinSquareExpectationS_all_axes_eq_of_axisSwapInvariant_zAxisRot | Problem 2.5.c concrete z-axis rotation input: constructs the general spin-S rotation exp(-iθŜ³), proves the -π/2 conjugation Ŝ² ↦ Ŝ¹, lifts it to a many-body single-site conjugation, and feeds it into PR #4060. The remaining input is invariance of the AFM ground state under the inverse lifted z-axis rotation, together with the existing lifted axis-swap invariance. Tasaki, Springer 2020, Problem 2.5.c, p. 43 and Theorem 2.4 context, pp. 43-44 (PR #4061, file Quantum/SpinS/Problem25cZAxisRotationInput.lean) |
| singleSiteSpinSquareExpectationS_eq_of_conj_phaseInvariant / _axis1_eq_axis2_of_unitaryPhaseInvariant / _all_axes_eq_of_axisSwapInvariant_unitary_phase_axis12 / _all_axes_eq_of_axisSwapInvariant_zAxisRot_phase | Problem 2.5.c phase-invariant axis input: weakens the exact unitary state-invariance hypotheses from PR #4057/PR #4060/PR #4061 to ray invariance T⁻¹Φ = c • Φ with star c * c = 1. This is the expected interface for deriving rotation invariance from one-dimensional AFM ground-state uniqueness: a commuting symmetry fixes the ground-state line up to phase, which is enough for squared expectations. Tasaki, Springer 2020, Problem 2.5.c, p. 43 and Theorem 2.4 context, pp. 43-44 (PR #4062, file Quantum/SpinS/Problem25cPhaseInvariantAxisInput.lean) |
| mulVec_eq_smul_of_finrank_eigenspace_le_one_of_commute / phase_unit_of_unitary_mulVec_eq_smul / exists_phase_unit_of_finrank_eigenspace_le_one_of_unitary_commute | Problem 2.5.c one-dimensional eigenspace phase bridge: in any finrank ≤ 1 Hamiltonian eigenspace, a non-zero eigenvector is fixed up to scalar by every commuting symmetry; if the symmetry is unitary and the eigenvector is normalized, the scalar satisfies star c * c = 1. This supplies the abstract ray-invariance and unit-modulus phase input expected by the PR #4062 wrappers; the remaining work is to prove the concrete lifted rotations commute with the AFM Hamiltonian. Tasaki, Springer 2020, Problem 2.5.c, p. 43 and Theorem 2.4 context, pp. 43-44 (PR #4063, file Quantum/SpinS/Problem25cEigenspacePhaseBridge.lean) |
| spinSRot3_eq_diagonal / manyBodyTensorS_spinSRot3_eq_exp_totalSpinSOp3 / heisenbergHamiltonianS_commute_manyBodySpinSRot3 | Problem 2.5.c lifted z-axis rotation commutation: identifies the tensor product z-axis rotation ⊗_x exp(-iθŜ³) with exp(-iθŜ_tot³) and combines this with [Ĥ_J, Ŝ_tot³] = 0 to prove that the spin-S Heisenberg Hamiltonian commutes with the lifted rotation. This supplies the concrete Hamiltonian-side commutation input for the one-dimensional eigenspace phase bridge. Tasaki, Springer 2020, Problem 2.5.c, p. 43 and Theorem 2.4 context, pp. 43-44 (PR #4064, file Quantum/SpinS/Problem25cZAxisRotationCommutation.lean) |
| manyBodySpinSRot3_conjTranspose_mul_self / exists_phase_unit_of_heisenbergHamiltonianS_manyBodySpinSRot3 / singleSiteSpinSquareExpectationS_all_axes_eq_of_axisSwapInvariant_zAxisRot_eigenphase | Problem 2.5.c z-axis ground-state phase input: proves the lifted z-axis rotation is unitary, specializes the one-dimensional eigenspace phase bridge to the Heisenberg Hamiltonian and the lifted π/2 z-rotation, and feeds the resulting unit-modulus phase into the existing squared-expectation wrapper. The lifted axis-swap state invariance remains an explicit hypothesis. Tasaki, Springer 2020, Problem 2.5.c, p. 43 and Theorem 2.4 context, pp. 43-44 (PR #4065, file Quantum/SpinS/Problem25cZAxisGroundStatePhase.lean) |
| axisSwappedAnisotropicHeisenbergS_one_zero / heisenbergHamiltonianS_commute_axisSwapUnitarySSpinS_tensorInv / exists_phase_unit_of_heisenbergHamiltonianS_axisSwapUnitarySSpinS_tensorInv / singleSiteSpinSquareExpectationS_all_axes_eq_of_zAxisRot_axisSwap_eigenphase | Problem 2.5.c axis-swap ground-state phase input: proves that the axis-swapped anisotropic Hamiltonian also reduces to the isotropic Heisenberg Hamiltonian at the SU(2) point λ = 1, D = 0, derives commutation and unit-modulus phase invariance for the inverse lifted axis-swap in any one-dimensional Heisenberg eigenspace, and combines it with the z-axis phase input to conclude all three squared single-site expectations without an explicit axis-swap state-invariance hypothesis. Tasaki, Springer 2020, Problem 2.5.c, p. 43 and Theorem 2.4 context, pp. 43-44 (PR #4066, files Quantum/SpinS/Problem25cAxisSwapGroundStatePhaseCore.lean for the axis-swap reduction, commutation and phase input + Quantum/SpinS/Problem25cAxisSwapGroundStatePhase.lean for the Problem 2.5.c squared-expectation wrappers, split for build speed) |
| singleSiteSpinSquareExpectationS_all_axes_eq_of_tasaki23_balanced_MLM_groundState | Problem 2.5.c MLM ground-state wrapper: combines PR #4066’s one-dimensional Heisenberg eigenspace squared-expectation wrapper with the balanced Marshall-Lieb-Mattis/SU(2) uniqueness endpoint from Theorem24SU2GlobalUniquenessFromMLM.lean. Under the balanced bipartite Theorem 2.3 hypotheses, any normalized non-zero Heisenberg eigenvector at the Hermitian minimum satisfies E_1 = E_2 = E_3 = N(N+2)/12. Tasaki, Springer 2020, Problem 2.5.c, p. 43 and Theorems 2.3-2.4, pp. 42-44 (PR #4067, file Quantum/SpinS/Problem25cMLMGroundStateWrapper.lean) |
| singleSiteSpinSquareExpectationS_all_axes_eq_of_balanced_bipartiteCompletePositive | Problem 2.5.c balanced structural wrapper: removes the explicit Theorem 2.3 witness from the MLM ground-state wrapper by invoking the structural Theorem 2.3 closure for balanced bipartite antiferromagnetic couplings. From the standard real symmetric non-negative bipartite hypotheses, complete-bipartite positivity, strict diagonal shift bounds for J and the toy coupling, balanced cardinalities, and 1 ≤ N, every normalized non-zero Heisenberg ground-state eigenvector satisfies E_1 = E_2 = E_3 = N(N+2)/12. Tasaki, Springer 2020, Problem 2.5.c, p. 43 and Theorems 2.3-2.4, pp. 42-44 (PR #4081, file Quantum/SpinS/Problem25cBalancedStructuralWrapper.lean) |
| twoSpinCorrelationS / bipartiteGaugeSign / twoSpinCorrelationS_sign_cases_of_bipartite_signed_re_pos | Problem 2.5.d correlation sign bridge: packages the final bipartite-gauge sign conversion in Tasaki’s solution. If the Marshall-gauge-signed two-spin correlation has positive real part, then the original correlation is positive on same-sublattice pairs and negative on cross-sublattice pairs. The remaining input is the Marshall-positive coefficient expansion that supplies the signed positivity hypothesis. Tasaki, Springer 2020, Problem 2.5.d, p. 40 and solution p. 498, equations (S.22)-(S.23) (PR #4068, file Quantum/SpinS/Problem25dCorrelationSignBridge.lean) |
| twoSpinPlusMinusCorrelationS / signedExpectation_re_eq_sum / signedExpectation_re_pos_of_positive_coefficients / twoSpinPlusMinusCorrelationS_bipartite_signed_re_pos_of_marshall_coefficients | Problem 2.5.d ladder positivity expansion: defines the ladder expectation ⟨Φ, Ŝ_x^+ Ŝ_y^- Φ⟩, expands a signed matrix expectation into the configuration-basis double sum, and proves that strictly positive Marshall-gauge coefficients plus non-negative signed matrix entries and one strictly positive entry imply positive signed ladder correlation. This packages the finite-sum positivity step behind Tasaki’s equation (S.23); the remaining input is the concrete Marshall-gauge matrix-entry non-negativity and strict witness for the ground-state vector. Tasaki, Springer 2020, Problem 2.5.d, p. 40 and solution p. 498, equations (S.22)-(S.23) (PR #4069, file Quantum/SpinS/Problem25dLadderPositivity.lean) |
| twoSpinPlusMinus_ladder_signed_entry_re_nonneg_of_bipartite_ne / exists_twoSpinPlusMinus_ladder_signed_entry_re_pos_of_bipartite_ne / twoSpinPlusMinusCorrelationS_bipartite_signed_re_pos_of_marshall_coefficients_cross | Problem 2.5.d ladder entry sign bridge: proves the concrete cross-sublattice Marshall-gauge sign input for Ŝ_x^+ Ŝ_y^-. For A x ≠ A y, the bipartite gauge sign and Marshall sign product cancel on every non-zero ladder matrix entry, leaving the bare non-negative entry; for N ≥ 1 an explicit two-configuration witness gives strict positivity. This feeds PR #4069’s finite-sum positivity wrapper for strictly positive Marshall coefficients. Tasaki, Springer 2020, Problem 2.5.d, p. 40 and solution p. 498, equations (S.22)-(S.23) (PR #4071, file Quantum/SpinS/Problem25dLadderEntrySign.lean) |
| twoSpinMinusPlusCorrelationS / twoSpinZZCorrelationS / twoSpinCorrelationS_eq_ladder_components / signed_twoSpinCorrelationS_re_pos_of_ladder_component_equalities / twoSpinCorrelationS_bipartite_signed_re_pos_of_marshall_cross_components | Problem 2.5.d ladder-to-dot reduction: lifts Ŝ_x · Ŝ_y = 1/2(Ŝ_x^+Ŝ_y^- + Ŝ_x^-Ŝ_y^+) + Ŝ_x^3Ŝ_y^3 to the two-spin correlation level and packages the conditional SU(2) sign transfer. If the signed Ŝ_x^-Ŝ_y^+ real part matches the signed Ŝ_x^+Ŝ_y^- real part and the signed longitudinal Ŝ_x^3Ŝ_y^3 real part is half of it, then signed ladder positivity implies signed dot-product positivity; combined with PR #4071 this gives the Marshall-coefficient cross-sublattice wrapper under those component equalities. Tasaki, Springer 2020, Problem 2.5.d, p. 40 and solution p. 498, equations (S.22)-(S.23) (PR #4072, file Quantum/SpinS/Problem25dLadderDotReduction.lean) |
| dotProduct_star_conjTranspose_mulVec_eq_star / twoSpinPlusMinus_ladder_conjTranspose / twoSpinMinusPlusCorrelationS_eq_star_twoSpinPlusMinusCorrelationS / bipartite_signed_twoSpinMinusPlusCorrelationS_re_eq_plusMinus / twoSpinCorrelationS_bipartite_signed_re_pos_of_marshall_cross_ladderAdjoint | Problem 2.5.d ladder adjoint equality: discharges the first component-equality input left by PR #4072. A generic adjoint-expectation bridge shows that the expectation of M† is the complex conjugate of the expectation of M; since (Ŝ_x^+Ŝ_y^-)† = Ŝ_x^-Ŝ_y^+ for x ≠ y, the two ladder expectations are complex conjugates, and multiplication by the real cross-sublattice bipartite gauge sign preserves equality of real parts. The resulting wrapper combines PR #4071 and PR #4072 while leaving only the longitudinal Ŝ_x^3Ŝ_y^3 equality as the remaining SU(2) input. Tasaki, Springer 2020, Problem 2.5.d, p. 40 and solution p. 498, equations (S.22)-(S.23) (PR #4073, file Quantum/SpinS/Problem25dLadderAdjointEquality.lean) |
| twoSpinProductCorrelationS / twoSpinProductCorrelationS_spinSOp3_eq_twoSpinZZCorrelationS / twoSpinProductCorrelationS_eq_of_conj_phaseInvariant / conj_product_of_conj_factors / twoSpinProductCorrelationS_axis3_eq_axis2_of_axisSwap_phase / twoSpinProductCorrelationS_axis1_eq_axis2_of_zAxisRot_phase / twoSpinProductCorrelationS_axis1_add_axis2_eq_ladder / bipartite_signed_twoSpinZZCorrelationS_re_eq_half_plusMinus_of_axis_phases / twoSpinCorrelationS_bipartite_signed_re_pos_of_marshall_cross_axis_phases | Problem 2.5.d longitudinal component equality: discharges the remaining longitudinal SU(2) component equality left by PR #4073 under axis-swap and z-axis rotation phase invariance. The two-site phase-invariant bridge gives C33 = C22 and C11 = C22; the spinSOp3 bridge identifies C33 with the existing twoSpinZZCorrelationS; the transverse ladder identity gives C11 + C22 = 1/2(C^{+-} + C^{-+}); PR #4073 gives equality of the signed ladder real parts, hence Re(g C33) = 1/2 Re(g C^{+-}). The resulting wrapper removes the final component-equality hypothesis from the signed dot-product positivity transfer. Tasaki, Springer 2020, Problem 2.5.d, p. 40 and solution pp. 498-499, equations (S.22)-(S.23) (PR #4074, files Quantum/SpinS/Problem25dLongitudinalComponentEqualityCore.lean for the phase-invariant bridges / axis equalities + Quantum/SpinS/Problem25dLongitudinalComponentEquality.lean for the longitudinal equality and Problem 2.5.d wrapper, split for build speed) |
| twoSpinCorrelationS_bipartite_signed_re_pos_of_marshall_cross_eigenphase / twoSpinCorrelationS_signed_re_pos_of_tasaki23_balanced_MLM_groundState | Problem 2.5.d ground-state phase wrapper: removes the explicit axis-swap and z-axis rotation phase hypotheses from PR #4074. A normalized non-zero Marshall-positive Heisenberg eigenvector in a one-dimensional eigenspace supplies both unit-modulus phases through the Problem 2.5.c ground-state phase bridges, and the balanced MLM/SU(2) endpoint supplies that one-dimensionality at the Hermitian minimum under the Theorem 2.3 hypotheses. This wrapper is for a full-space coefficient function; the sector-supported Perron-Frobenius ground-state shape is handled separately. Tasaki, Springer 2020, Problem 2.5.d, p. 40 and solution pp. 498-499, equations (S.22)-(S.23), with Theorems 2.3-2.4 context, pp. 42-44 (PR #4075, file Quantum/SpinS/Problem25dGroundStatePhaseWrapper.lean) |
| twoSpinPlusMinusCorrelationS_bipartite_signed_re_pos_of_marshall_sector_coefficients / twoSpinPlusMinusCorrelationS_bipartite_signed_re_pos_of_marshall_sector_cross / twoSpinCorrelationS_bipartite_signed_re_pos_of_marshall_sector_cross_components / twoSpinCorrelationS_bipartite_signed_re_pos_of_marshall_sector_cross_axis_phases / twoSpinCorrelationS_bipartite_signed_re_pos_of_marshall_sector_cross_eigenphase | Problem 2.5.d sector-supported wrapper: adapts the PR #4069–#4075 positivity chain to the actual sector-supported Marshall-positive ground-state shape produced by Perron-Frobenius. A sector vector with strictly positive coefficients is zero-extended by magSectorEmbedding; off-sector terms in the ladder expectation vanish, on-sector terms are positive-coefficient multiples of the signed matrix entries, and the same axis-phase/eigenspace bridge supplies the signed dot-product positivity conclusion. Tasaki, Springer 2020, Problem 2.5.d, p. 40 and solution pp. 498-499, equations (S.22)-(S.23), with Theorems 2.3-2.4 context, pp. 42-44 (PR #4076, file Quantum/SpinS/Problem25dSectorSupportedWrapper.lean) |
← Spin-S Marshall–Lieb–Mattis on the magnetization sector (Tasaki §2.5 Theorem 2.2 generic S, sector form) · Catalogue · Spin-S saturated ferromagnetic state (Tasaki §2.4 generalised) →