S Marshall–Lieb–Mattis on the magnetization sector (Tasaki §2.5 Theorem 2.2 generic S, sector form) (part 1 of 4)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 Marshall–Lieb–Mattis on the magnetization sector (Tasaki §2.5 Theorem 2.2 generic S, sector form)Route correction (2026-05-26). The earlier “saturated-ladder-iterate” route toward
tasaki_2_5_theorem_2_3was found unsound: it reduced the theorem to a leaf hypothesis (lowerable attach-sum dominance) that is false — the ferromagnetic ladder iterate(Ŝ⁻_tot)^M|all-up⟩is not the Marshall-positive antiferromagnetic ground state (concrete counterexample: spin-1/2,V={a,b},A={a},B={b},M=0→1). The 40 conditional-wrapper modules of that route were removed; their detailed rows below were deleted with them. The sound route keeps the per-sector Perron–Frobenius ground state (marshallLiebMattis_spinS_heisenbergHamiltonianS_groundState_full, sorry-free) and chains sectors by SU(2) invariance[Ĥ, Ŝ⁻_tot] = 0. The rows below that still name helper lemmas from the removed route now carry an explicit deletion note on the dead name (deleted in PR #3645 (unsound saturated-ladder Theorem 2.3 route), ordeleted in PR #3919 (bulk orphan-module deletion)for names that outlived that route and went with the later bulk deletion); the Deleted routes section above lists the deleted variant families. See.self-local/docs/tasaki-2-5-pf-route-design.mdand Issue #3542.
Generic-spin (N = 2S) version of Tasaki §2.5 Theorem 2.2 applied to the
magnetization-M sector of the un-dressed antiferromagnetic
Heisenberg Hamiltonian on a bipartite graph. The sector subtype
magConfigS V N M := { σ : V → Fin (N + 1) // magSumS σ = M } is the
natural index type since the dressed Heisenberg matrix is irreducible
on each sector. The core sector-matrix API lives in
Quantum/SpinS/DressedMatrixOnMagSector.lean; the trailing
eigenvalue-uniqueness + complex-form MLM Theorem 2.2 statements
were moved to the companion
Quantum/SpinS/DressedMatrixOnMagSectorEigenvalueUnique.lean in
refactor #30 (PR #2829). The two bundled sector-level MLM Theorem 2.2
ground-state results (marshallLiebMattis_spinS_heisenbergSector_groundState,
marshallLiebMattis_spinS_heisenbergSector_complexGroundState_full) were
subsequently relocated to
Quantum/SpinS/MarshallLiebMattisSectorBundled.lean (#4569, re-proved via the
canonical *Structural* twins). Tracked in Issue #412.
| Lean name | Statement |
|—|—|
| tasaki23_pf_ladder_link_succ | Sound PF adjacent-sector ladder link (lowering): if a magnetization-M sector vector magSectorEmbedding Φ is a Heisenberg eigenvector at energy μ and a total-Casimir eigenvector at γ away from the sector’s lowering-kernel value (card·N/2−M)(card·N/2−M−1), then Ŝ⁻_tot · magSectorEmbedding Φ is a Heisenberg eigenvector at the same μ (via [Ĥ, Ŝ⁻_tot]=0), is non-zero (total-Casimir non-vanishing criterion), and lies in the next magnetization sector. This is the energy-preserving step that chains the per-sector Perron–Frobenius ground states (marshallLiebMattis_spinS_heisenbergHamiltonianS_groundState_full) across the admissible range; it uses no Marshall positivity of the lowered vector (the false hypothesis of the removed ferromagnetic-ladder route). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23PFLadderLink.lean) |
| tasaki23_pf_ladder_link_pred / tasaki23_pf_ladder_link_pred_of_mem_predictedGS | Sound PF adjacent-sector ladder link (raising) and its predicted-GS specialisation: the raising companions of tasaki23_pf_ladder_link_succ(_of_mem_predictedGS). Ŝ⁺_tot maps a sector-K Heisenberg eigenvector (total-Casimir away from the raising-kernel value (card·N/2−K)(card·N/2−K+1)) to a non-zero same-energy eigenvector in the previous sector; predicted-GS membership in sector M+1 strictly above the left endpoint discharges the Casimir hypotheses via tasaki23_predictedCasimirValue_ne_raising_kernel_value_of_mem_of_left_lt. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23PFLadderLink.lean) |
| sublatticeMagSubspaceS / sublatticeMagEigenvalueS (with mem_sublatticeMagSubspaceS_iff, basisVecS_mem_sublatticeMagSubspaceS, sublatticeMagSubspaceS_disjoint) | Sublattice magnetization grading: the Ŝ_A^(3)-eigenspaces sublatticeMagSubspaceS A M and the diagonal eigenvalue sublatticeMagEigenvalueS A σ = ∑_{x∈A}(N/2−σ_x). Disjointness of distinct eigenvalues and basis-state membership (Submodule membership uses mathlib’s standard .zero_mem/.add_mem/.smul_mem/… directly — no dedicated wrapper lemmas). Sublattice analogue of magSubspaceS/magEigenvalueS; scaffold (Issue #3658, PR 5) for the sublattice highest-weight argument bounding (Ŝ_A)². Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeMagnetization.lean) |
| tasaki23_toy_groundState_sublattice_casimir_re_le | Sublattice Casimir bounds for the toy ground state: the per-sector Marshall-positive toy GS is a joint Casimir eigenvector (#3657) whose (Ŝ_A)²/(Ŝ_¬A)² eigenvalues γ_A, γ_B obey γ_A.re ≤ s_A(s_A+1), γ_B.re ≤ s_B(s_B+1) (apply the spectral max bound #3672 to the non-zero Marshall-dressed embedding). Discharges two hypotheses of the toy total-Casimir pin #3676 (Issue #3674, PR 3). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23StructuralPFJointCasimir.lean) |
| tasaki23_extremal_sector_magnetization_re_eq_predicted | Extremal sector realizes the predicted total spin: for the left-endpoint sector M = min(|A|,|¬A|)·N, the magnetization eigenvalue |V|·N/2 − M has real part = tasaki23PredictedTotalSpin A N = |s_A − s_B|. Supplies the extremal-sector hypothesis hM of the toy total-Casimir pin #3676 (Issue #3674, PR 4). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23ExtremalSector.lean) |
| tasaki23_toy_groundState_casimir_eq_predicted_of_energy_le | Toy ground state is the predicted-Casimir witness (modulo the energy bound): in the extremal sector M = min(|A|,|¬A|)·N, the Marshall-positive toy GS with toy energy μ ≤ predicted − s_A(s_A+1) − s_B(s_B+1) is a (Ŝ_tot)²-eigenvector at exactly tasaki23PredictedCasimirValue A N. Capstone assembling the joint eigenvector (#3657), sublattice bounds (#3677), toy energy formula (#3673), extremal sector (#3678), the two-sided pin (#3676), and Hermitian eigenvalue realness — exactly the witness form required by #3656. The single remaining obligation is the reference energy bound hμ (Issue #3674, PR 5). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23ToyWitness.lean) |
| tasaki23_toy_sector_groundEnergy_le_of_witness | Toy ground energy is minimal in its sector: the Marshall-positive toy ground state (energy μ) has μ ≤ E for every sector eigenvector φ ≠ 0 of the toy Heisenberg sector matrix at real energy E. Specialises heisenbergHamiltonianSReMatrixOnMagSector_eigenvalue_ge_of_marshallPositive to J = bipartiteCoupling A; reduces the reference energy bound hμ (and hence the whole route, via #3679) to exhibiting one sector eigenvector at the predicted ground energy predicted − s_A(s_A+1) − s_B(s_B+1) (Issue #3674, PR 6). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23ToyGroundEnergyBound.lean) |
| tasaki23_total_casimir_re_eq_predicted_of_bounds (with tasaki23PredictedTotalSpin_nonneg) | Toy total-Casimir pin (extremal sector): in the extremal magnetization sector M.re = |s_A−s_B|, a non-zero (Ŝ_tot)²-eigenvector at γ_tot with sublattice Casimir max bounds γ_A ≤ s_A(s_A+1), γ_B ≤ s_B(s_B+1) and reference toy energy bound (γ_tot−γ_A−γ_B).re ≤ predicted − s_A(s_A+1) − s_B(s_B+1) has γ_tot.re = predicted. A two-sided squeeze (magnetization lower bound #3675 + sublattice upper bounds #3672 + energy formula #3673), isolating the extremal-sector and reference-energy obligations as hypotheses; no Clebsch–Gordan (Issue #3674, PR 2). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23ToyCasimirPin.lean) |
| totalSpinSSquared_eigenvalue_re_ge_of_mem_magSubspaceS (with exists_highestWeight_eigenvector_ge) | Total-Casimir magnetization lower bound (Ŝ_tot)² ≥ m(m+1): a non-zero (Ŝ_tot)²-eigenvector at γ in magSubspaceS V N M with 0 ≤ M.re has M.re·(M.re+1) ≤ γ.re. The total spin dominates its z-projection: raising with Ŝ⁺_tot only increases the magnetization, so the highest weight M' reached has M' ≥ M, giving γ = M'(M'+1) ≥ M(M+1). Lower-bound companion of totalSpinSSquared_eigenvalue_re_le_sMax; in the extremal sector m = s_A−s_B it pins the toy GS total Casimir to predicted, bypassing the Clebsch–Gordan triangle inequality (Issue #3674, PR 1). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/CasimirSpectralLowerBound.lean) |
| heisenbergToyHamiltonianS_mulVec_of_joint_casimir_eigenvector | Toy energy on a joint Casimir eigenvector: a simultaneous eigenvector of (Ŝ_tot)², (Ŝ_A)², (Ŝ_¬A)² at (γ_tot, γ_A, γ_B) is a Ĥ_toy-eigenvector at γ_tot − γ_A − γ_B (from Ĥ_toy = (Ŝ_tot)²−(Ŝ_A)²−(Ŝ_¬A)²). The energy formula underlying the variational identification of the toy ground state’s predicted total Casimir (Issue #3658, PR 4 step 1). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/ToyHamiltonianJointEnergy.lean) |
| sublatticeSpinSquaredS_eigenvalue_re_le_sA | Sublattice Casimir spectral max bound (Ŝ_A)² ≤ s_A(s_A+1): every eigenvalue γ of (Ŝ_A)² (with a non-zero eigenvector) has γ.re ≤ s_A(s_A+1), s_A = |A|·N/2. Assembles the sublattice weight-component extraction (#3670), highest-weight existence (#3671), and the highest-weight bound (#3668). Sublattice analogue of totalSpinSSquared_eigenvalue_re_le_sMax; the sublattice analytic ingredient of the Issue #3658 witness construction (Issue #3658, PR 12). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeCasimirSpectralBound.lean) |
| sublatticeExists_highestWeight_eigenvector (with sublatticeMagEigenvalueS_ne_sMax_add_one) | Sublattice highest-weight existence: from a non-zero (Ŝ_A)²-eigenvector at γ in sublatticeMagSubspaceS A (s_A−k), repeatedly raising with Ŝ_A^+ (which terminates once the sublattice magnetization exceeds s_A, since the subspace at s_A+1 is ⊥) produces a non-zero highest-weight (Ŝ_A)²-eigenvector at the same γ. Sublattice analogue of exists_highestWeight_eigenvector (Issue #3658, PR 11). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeHighestWeightExistence.lean) |
| sublatticeSpinSquaredS_eigenvec_exists_weight_component (with sublatticeSpinSquaredS_mulVec_sublatticeMagProjFn_eq, sublatticeSpinSquaredS_mulVec_mem_sublatticeMagSubspaceS) | Sublattice weight-component extraction: since (Ŝ_A)² commutes with Ŝ_A^(3) it preserves each sublattice magnetization subspace and commutes with the projector; hence a non-zero (Ŝ_A)²-eigenvector at γ has a non-zero sublattice-weight component sublatticeMagProjFn A (s_A−k) v that is again a (Ŝ_A)²-eigenvector at γ in a single sublattice magnetization subspace. Sublattice analogue of totalSpinSSquared_eigenvec_exists_weight_component (Issue #3658, PR 10). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeMagWeightComponent.lean) |
| sublatticeMagProjFn / sum_sublatticeMagProjFn_eq (with sublatticeMagSumS, sublatticeMagEigenvalueS_eq_sub, sublatticeMagProjFn_mem_sublatticeMagSubspaceS) | Sublattice magnetization projection & decomposition: the pointwise projector sublatticeMagProjFn A M v (keeps v σ where sublatticeMagEigenvalueS A σ = M) lands in sublatticeMagSubspaceS A M, is linear, and the projectors over the finite spectrum s_A − k (k=0..|A|·N) sum to the identity (sublatticeMagEigenvalueS A σ = s_A − sublatticeMagSumS A σ, sublatticeMagSumS A σ = ∑_{x∈A}σ_x ≤ |A|·N). Sublattice analogue of magProjFn/sum_magProjFn_eq (Issue #3658, PR 9). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeMagProjection.lean) |
| sublatticeSpinSquaredS_highestWeight_eigenvalue_re_le (with sublatticeMagEigenvalueS_im_zero) | Sublattice highest-weight Casimir bound: a non-zero highest-weight (Ŝ_A)²-eigenvector (Ŝ_A^+ w = 0) at γ in sublatticeMagSubspaceS A M satisfies γ.re ≤ s_A(s_A+1), s_A = |A|·N/2. Its Casimir value is M(M+1) (#3663), M is an attained basis eigenvalue (#3667 ⊥-lemma), so |M| ≤ s_A (#3660). Sublattice analogue of totalSpinSSquared_highestWeight_eigenvalue_re_le (Issue #3658, PR 8). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeCasimirHighestWeightBound.lean) |
| sublatticeSpinSOp3_apply_diag / sublatticeSpinSOp3_apply_off_diag / sublatticeMagSubspaceS_eq_bot_of_not_in_spectrum | Sublattice magnetization spectrum: Ŝ_A^(3) is diagonal with entry sublatticeMagEigenvalueS A σ on the diagonal and zero off it; hence a value M outside the diagonal spectrum gives sublatticeMagSubspaceS A M = ⊥. Sublattice analogue of totalSpinSOp3_apply_diag/off_diag and magSubspaceS_eq_bot_of_not_in_spectrum; lets the highest-weight argument conclude an attained sublattice magnetization is an actual basis eigenvalue (so |M| ≤ s_A) (Issue #3658, PR 7). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeMagSpectrum.lean) |
| sublatticeSpinSOpPlus_mulVec_mem_sublatticeMagSubspaceS_of_mem / sublatticeSpinSOpMinus_mulVec_mem_sublatticeMagSubspaceS_of_mem | Sublattice ladder shifts the sublattice grading: Ŝ_A^+ maps sublatticeMagSubspaceS A M → A (M+1) and Ŝ_A^- maps it to A (M−1), from the grading commutators [Ŝ_A^(3), Ŝ_A^±] = ±Ŝ_A^±. Sublattice analogue of totalSpinSOpPlus_mulVec_mem_magSubspaceS_of_mem; drives the termination of the highest-weight raising for (Ŝ_A)² (Issue #3658, PR 6). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeMagShift.lean) |
| sublatticeSpinSquaredS_mulVec_of_sublatticeSpinSOpPlus_eq_zero | Sublattice highest-weight Casimir relation: if Ŝ_A^(3) w = m_A·w and Ŝ_A^+ w = 0, then (Ŝ_A)² w = m_A(m_A+1)·w. From the sublattice Cartan identity Ŝ_A^- Ŝ_A^+ = (Ŝ_A^1)²+(Ŝ_A^2)²−Ŝ_A^(3) (so (Ŝ_A)² = Ŝ_A^-Ŝ_A^+ + Ŝ_A^(3) + (Ŝ_A^(3))²); on a highest-weight Ŝ_A^(3)-eigenvector the Ŝ_A^-Ŝ_A^+ term vanishes. Sublattice analogue of the total highest-weight relation; scaffold (Issue #3658, PR 4) for the sublattice Casimir spectral max bound. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeHighestWeight.lean) |
| sublatticeSpinSquaredS_mulVec_of_sublatticeSpinSOpMinus_eq_zero | Sublattice lowest-weight Casimir relation: if Ŝ_A^(3) w = m_A·w and Ŝ_A^- w = 0, then (Ŝ_A)² w = m_A(m_A−1)·w. From the other sublattice Cartan identity Ŝ_A^+ Ŝ_A^- = (Ŝ_A^1)²+(Ŝ_A^2)²+Ŝ_A^(3) (so (Ŝ_A)² = Ŝ_A^+Ŝ_A^- − Ŝ_A^(3) + (Ŝ_A^(3))²); on a lowest-weight vector the Ŝ_A^+Ŝ_A^- term vanishes. At m_A = −s_A this gives (Ŝ_A)² = s_A(s_A+1) (max), so the all-down sublattice state realizes the maximal (Ŝ_A)² — a building block of the minimal-total-spin state (Issue #3674). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeLowestWeight.lean) |
| sublatticeSpinSquaredS_antiAligned_eq_max / sublatticeSpinSquaredS_complement_antiAligned_eq_max (with antiAlignedConfigS) | Anti-aligned state realizes the maximal sublattice Casimirs: the basis config antiAlignedConfigS A N (all A-sites up σ=0, all ¬A-sites down σ=N) satisfies (Ŝ_A)² |σ₀⟩ = s_A(s_A+1) |σ₀⟩ and (Ŝ_¬A)² |σ₀⟩ = s_B(s_B+1) |σ₀⟩ — the A-block is the sublattice highest weight (#3663), the ¬A-block the sublattice lowest weight (#3681). Total magnetization s_A − s_B (the extremal sector); projecting onto (Ŝ_tot)²=predicted yields the minimal-total-spin state (Issue #3674, PR 8). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23AntialignedJointEigenvector.lean) |
| tasaki23_extremal_highestWeight_totalCasimir_eq_predicted | Extremal-sector highest weight has the predicted total Casimir: a vector in the extremal magnetization sector M = min(|A|,|¬A|)·N annihilated by Ŝ⁺_tot is a (Ŝ_tot)²-eigenvector at exactly tasaki23PredictedCasimirValue A N (the total highest-weight relation gives m(m+1) with m = |s_A−s_B|, via #3678). With the maximal sublattice Casimirs, such a highest-weight vector is the minimal-total-spin joint eigenstate; its existence (Clebsch–Gordan) is the last obligation (Issue #3674, PR 9). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23ExtremalHighestWeight.lean) |
| jointSublatticeCasimirEigenspace_totalSpinSOpPlus_invariant / _totalSpinSOpMinus_invariant | Ladder invariance of the joint sublattice-Casimir eigenspace: W = jointSublatticeCasimirEigenspace A N ((Ŝ_A)²=s_A(s_A+1) and (Ŝ_¬A)²=s_B(s_B+1)) is invariant under Ŝ⁺_tot and Ŝ⁻_tot (both sublattice Casimirs commute with them). W is the carrier on which (Ŝ_tot)² decomposes; the rank-nullity of Ŝ⁺_tot across its magnetization grading yields the minimal-total-spin highest-weight state (Issue #3674, PR 10). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/JointCasimirEigenspaceLadderInvariant.lean) |
| jointSublatticeCasimirEigenspace_totalSpinSOp3_invariant | Ŝ³_tot-invariance of the joint sublattice-Casimir eigenspace: W = jointSublatticeCasimirEigenspace A N is invariant under Ŝ³_tot (both sublattice Casimirs commute with it), so it is graded by total magnetization W = ⊕_M (W ⊓ magSubspaceS V N M). With the ladder invariance (#3684), W is an su(2)-subrepresentation — the setting for the rank-nullity argument producing the minimal-total-spin highest-weight state (Issue #3674, PR 11). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/JointCasimirEigenspaceMagInvariant.lean) |
| sublatticeMaxCasimirEigenspace_ne_bot (with allAlignedStateS_zero_mem_sublatticeMaxCasimirEigenspace) | The maximal sublattice-Casimir eigenspace is non-trivial: the (Ŝ_A)²-eigenspace at s_A(s_A+1) (the A-symmetric subspace) contains the non-zero all-up state |σ_⊤⟩. Sublattice analogue of totalSpinSSquaredEigenspace_max_ne_bot; the base of the sublattice-symmetric-subspace dimension theory producing the minimal-total-spin highest-weight state (Issue #3687, PR 1). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeMaxCasimirEigenspaceNeBot.lean) |
| sublatticeMaxCasimirEigenspace_complement_ne_bot | The complement maximal sublattice-Casimir eigenspace is non-trivial: the (Ŝ_¬A)²-eigenspace at s_B(s_B+1) contains the non-zero all-up state. Complement companion of sublatticeMaxCasimirEigenspace_ne_bot, via the negated sublattice (Issue #3687, PR 2). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeMaxCasimirEigenspaceComplementNeBot.lean) |
| sublatticeMaxCasimirEigenspace_sublatticeSpinSOpMinus_invariant / _sublatticeSpinSOpPlus_invariant | Ladder invariance of the maximal sublattice-Casimir eigenspace: the (Ŝ_A)²-eigenspace (any eigenvalue M) is invariant under the sublattice ladders Ŝ_A^+, Ŝ_A^- (the sublattice Casimir commutes with them). With non-triviality (#3688), the A-symmetric subspace contains the whole Ŝ_A^--ladder orbit of the all-up state — its spanning set with one state per A-magnetization (Issue #3687, PR 3). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeMaxCasimirEigenspaceLadderInvariant.lean) |
| sublatticeLadderIterateDownS / sublatticeSpinSquaredS_mulVec_sublatticeLadderIterateDownS | Sublattice ladder iterates of the all-up state: (Ŝ_A^-)^k · |σ_⊤⟩ lies in the maximal (Ŝ_A)²-eigenspace ((Ŝ_A)² commutes with every power of Ŝ_A^-, and |σ_⊤⟩ realizes the maximal Casimir). These iterates (one per A-magnetization) are the spanning family of the A-symmetric subspace; sublattice analogue of ladderIterateUp (§2.4) (Issue #3687, PR 4). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeLadderIterate.lean) |
| sublatticeLadderIterateDownS_mem_sublatticeMagSubspaceS (with sublatticeMagEigenvalueS_allUp) | Sublattice magnetization of the ladder iterates: (Ŝ_A^-)^k · |σ_⊤⟩ ∈ sublatticeMagSubspaceS A (s_A − k) (the all-up state has Ŝ_A^(3)-eigenvalue s_A, and each Ŝ_A^- lowers the sublattice magnetization by one). Distinct k give distinct sublattice magnetizations, so the iterates are linearly independent once non-vanishing is established — the dimension-counting input for the A-symmetric subspace (Issue #3687, PR 5). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeLadderIterateMag.lean) |
| sublatticeSpinSOpPlus_mulVec_sublatticeLadderIterateDownS_succ | Sublattice raising-of-lowering identity: Ŝ_A^+ (Ŝ_A^-)^{k+1} \|σ_⊤⟩ = (k+1)(\|A\|·N − k) (Ŝ_A^-)^k \|σ_⊤⟩. The su(2) ladder identity for the A-sublattice on the all-up state, from the sublattice Cartan Ŝ_A^+ Ŝ_A^- = (Ŝ_A)² − (Ŝ_A^(3))² + Ŝ_A^(3), the maximal Casimir (#3691) and the iterate’s magnetization s_A − k (#3692). Since (k+1)(\|A\|·N − k) ≠ 0 for k < \|A\|·N, it drives the inductive non-vanishing of the iterates; sublattice analogue of §2.4’s total identity (Issue #3687, PR 6). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeLadderIdentity.lean) |
| sublatticeLadderIterateDownS_ne_zero | Non-vanishing of the sublattice ladder iterates: for k ≤ |A|·N, (Ŝ_A^-)^k · |σ_⊤⟩ ≠ 0. Inductive (sublattice analogue of §2.4’s total non-vanishing): if v_{k+1}=0 then Ŝ_A^+ v_{k+1} = (k+1)(|A|·N−k) v_k = 0 (the ladder identity #3693), and the scalar is non-zero for k < |A|·N, forcing v_k = 0 against the IH. With the distinct magnetizations (#3692), the |A|·N+1 iterates are linearly independent (Issue #3687, PR 7). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeLadderIterateNonvanishing.lean) |
| sublatticeLadderIterateDownFin_linearIndependent (with sublatticeLadderEigenvalueDown, sublatticeLadderIterateDownFin) | Linear independence of the sublattice ladder family: the iterates (Ŝ_A^-)^k · |σ_⊤⟩ for k = 0,…,|A|·N are linearly independent — each is a non-zero Ŝ_A^(3)-eigenvector (#3694, #3692) at the distinct eigenvalue s_A − k, and eigenvectors at distinct eigenvalues are LI (Module.End.eigenvectors_linearIndependent'). Hence finrank of the A-symmetric subspace is ≥ |A|·N+1; sublattice analogue of ladderIterateUp_linearIndependent (§2.4) (Issue #3687, PR 8). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeLadderLI.lean) |
| sublatticeMaxCasimirEigenspace_finrank_ge (with sublatticeLadderIterateDownFin_mem_maxCasimirEigenspace) | Lower bound on the A-symmetric subspace dimension: |A|·N+1 ≤ finrank((Ŝ_A)²-eigenspace at s_A(s_A+1)), from the |A|·N+1 linearly-independent ladder iterates (#3691 membership + #3695 LI). Sublattice analogue of totalSpinSSquared_eigenspace_finrank_ge_succ_card_mul_N (§2.4) (Issue #3687, PR 9). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeMaxCasimirFinrankGe.lean) |
| sublatticeMaxCasimirEigenspace_complement_finrank_ge | Lower bound on the ¬A-symmetric subspace dimension: |¬A|·N+1 ≤ finrank((Ŝ_¬A)²-eigenspace at s_B(s_B+1)), by applying the A-version to the negated sublattice (Issue #3687, PR 10). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeMaxCasimirFinrankGeComplement.lean) |
| jointLadderIterateDownS / sublatticeSpinSquaredS_mulVec_jointLadderIterateDownS / sublatticeSpinSquaredS_complement_mulVec_jointLadderIterateDownS | Joint two-sublattice ladder iterates: (Ŝ_A^-)^{k_A} (Ŝ_¬A^-)^{k_B} · |σ_⊤⟩ lies in the joint maximal-Casimir eigenspace W ((Ŝ_A)²=s_A(s_A+1) and (Ŝ_¬A)²=s_B(s_B+1)): each sublattice Casimir commutes with the product of ladder powers (same-sublattice + cross-sublattice complement commute) and |σ_⊤⟩ realizes both maximal Casimirs. The spanning family of W (one per (A,¬A)-magnetization pair) (Issue #3687, PR 11). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/JointLadderIterate.lean) |
| jointLadderIterateDownS_mem_magSubspaceS (with sublatticeSpinSOpMinus_pow_mulVec_mem_magSubspaceS) | Total magnetization of the joint iterate: (Ŝ_A^-)^{k_A} (Ŝ_¬A^-)^{k_B} · |σ_⊤⟩ ∈ magSubspaceS V N (|V|·N/2 − (k_A + k_B)) — each total ladder lowering drops the total magnetization by one. Within a fixed total magnetization the joint iterates are distinguished by their A-magnetization; the dimension input for the rank–nullity argument (Issue #3687, PR 12). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/JointLadderIterateMag.lean) |
| jointLadderIterateDownS_mem_sublatticeMagSubspaceS (with sublatticeSpinSOp3_cross_commute_sublatticeSpinSOpMinus) | A-magnetization of the joint iterate: (Ŝ_A^-)^{k_A} (Ŝ_¬A^-)^{k_B} · |σ_⊤⟩ ∈ sublatticeMagSubspaceS A (s_A − k_A) — Ŝ_¬A^- preserves the A-magnetization (commutes with Ŝ_A^(3)) and each Ŝ_A^- drops it by one. Distinct k_A give distinct A-magnetizations, yielding (with non-vanishing) the linear independence of the diagonal family (Issue #3687, PR 13). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/JointLadderIterateSublatticeMag.lean) |
| sublatticeSpinSOpPlus_mulVec_jointLadderIterateDownS_succA | Raising the A-index of the joint iterate: Ŝ_A^+ · jointIterate (k_A+1) k_B = (k_A+1)(\|A\|·N − k_A) · jointIterate k_A k_B. Generalizes the single-sublattice ladder identity (#3693) to the joint iterate via the joint maximal A-Casimir (#3698) and A-magnetization s_A − k_A (#3700). Shows Ŝ_A^+ maps the diagonal family into the lower-index family — half of the rank–nullity step (Issue #3687, PR 14). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/JointLadderRaiseA.lean) |
| sublatticeSpinSOpPlus_complement_mulVec_jointLadderIterateDownS_succB | Raising the ¬A-index of the joint iterate: Ŝ_¬A^+ · jointIterate k_A (k_B+1) = (k_B+1)(\|¬A\|·N − k_B) · jointIterate k_A k_B. Complement companion of #3701: Ŝ_¬A^+ commutes past (Ŝ_A^-)^{k_A} (cross-sublattice) and the inner single-sublattice ladder identity (#3693 at ¬A) lowers the ¬A-index. With #3701, Ŝ⁺_tot = Ŝ_A^+ + Ŝ_¬A^+ maps the diagonal family into the lower-index family — the rank–nullity step (Issue #3687, PR 15). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/JointLadderRaiseB.lean) |
| jointLadderIterateDownS_ne_zero | Non-vanishing of the joint ladder iterates: for k_A ≤ |A|·N, k_B ≤ |¬A|·N, (Ŝ_A^-)^{k_A} (Ŝ_¬A^-)^{k_B} · |σ_⊤⟩ ≠ 0. Induction on k_A (base = ¬A-iterate non-vanishing #3694; step via the A-raising identity #3701 with non-zero scalar for k_A < |A|·N). With the joint A-magnetization (#3700), the diagonal-family members are non-zero eigenvectors at distinct A-magnetizations, hence linearly independent (Issue #3687, PR 16). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/JointLadderIterateNonvanishing.lean) |
| jointDiagonalIterate / jointDiagonalIterate_linearIndependent | Linear independence of the diagonal joint-ladder family: at the extremal total magnetization s_A − s_B (WLOG |¬A| ≤ |A|), the diagonal family k_A ↦ jointLadderIterateDownS A N k_A (|¬A|·N − k_A) (k_A = 0,…,|¬A|·N) is linearly independent — each member is a non-zero Ŝ_A^(3)-eigenvector (#3703, #3700) at the distinct eigenvalue s_A − k_A. This (|¬A|·N+1)-element family in W ∩ mag-(s_A−s_B) is the source of the rank–nullity argument (Issue #3687, PR 17). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/JointDiagonalLI.lean) |
| sublatticeSpinSOpPlus_mulVec_jointLadderIterateDownS_zeroA / _complement_mulVec_jointLadderIterateDownS_zeroB | Boundary annihilation under raising: Ŝ_A^+ kills jointIterate 0 k_B (A-block fully up) and Ŝ_¬A^+ kills jointIterate k_A 0 (¬A-block fully up) — each total raising operator commutes the ladder past (Ŝ^-) powers and annihilates the all-up state. With the interior raising identities (#3701, #3702), Ŝ⁺_tot maps the diagonal family into the lower-index family (Issue #3687, PR 18). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/JointLadderRaiseBoundary.lean) |
| totalSpinSOpPlus_mulVec_jointDiagonalIterate_mem_span (with jointLowerDiagonalIterate) | Ŝ⁺_tot maps the diagonal family into the lower-index span: Ŝ⁺_tot · jointDiagonalIterate A N k_A ∈ span(range(jointLowerDiagonalIterate A N)). Splitting Ŝ⁺_tot = Ŝ_A^+ + Ŝ_¬A^+, the A-raising (#3701/#3705) and ¬A-raising (#3702/#3705) identities send each diagonal member to a scalar multiple of a lower-index member (or 0). Since M+1 diagonal vectors land in the ≤M-dimensional lower span, the rank–nullity argument yields a non-trivial Ŝ⁺_tot-kernel (Issue #3687, PR 19). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/JointDiagonalRaiseImage.lean) |
| exists_jointDiagonal_totalSpinSOpPlus_kernel | Non-trivial Ŝ⁺_tot-kernel in the diagonal span (rank–nullity, for |¬A| ≤ |A|): there is a non-zero w ∈ span(range(jointDiagonalIterate A N)) with Ŝ⁺_tot w = 0. The M+1 linearly-independent diagonal iterates (#3704) map under Ŝ⁺_tot into the ≤M-dimensional lower span (#3706, finrank_span_le_card + fintype_card_le_finrank), so the images are linearly dependent; the witnessing combination w = ∑ c_{k_A}·jointDiagonalIterate is non-zero (diagonal LI) and Ŝ⁺_tot-killed. This w is the minimal-total-spin highest-weight state (Issue #3687, PR 20). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/JointDiagonalKernel.lean) |
| exists_jointPredictedCasimir_eigenvector (with jointDiagonalIterate_mem_jointSublatticeCasimirEigenspace, jointDiagonalIterate_mem_magSubspaceS) | The minimal-total-spin joint predicted-Casimir eigenvector exists (for |¬A| ≤ |A|): a non-zero vector that is a simultaneous eigenvector of (Ŝ_tot)² (at tasaki23PredictedCasimirValue), (Ŝ_A)² (at s_A(s_A+1)) and (Ŝ_¬A)² (at s_B(s_B+1)). The rank–nullity kernel w (#3707) lies in the joint Casimir eigenspace W (#3698) and the extremal sector (#3699), so by the extremal highest-weight relation (#3683) (Ŝ_tot)² w = predicted. This is the witness the toy-ground-state route needs (Issue #3687, PR 21). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/JointDiagonalPredictedEigenvector.lean) |
| exists_jointPredictedCasimir_witness, exists_predictedEnergy_sector_eigenvector | A real sector eigenvector at the predicted toy energy (for |¬A| ≤ |A|): the minimal-total-spin joint eigenvector (#3709) is a full-space heisenbergHamiltonianS (bipartiteCoupling A)-eigenvector at the predicted toy energy E = predicted − s_A(s_A+1) − s_B(s_B+1) (via heisenbergToyHamiltonianS = heisenbergHamiltonianS (bipartiteCoupling A) and the Casimir energy formula #3673); restricting it to the extremal sector M = |¬A|·N and taking real/imaginary parts (real coupling, bipartiteCoupling_im) yields a non-zero real eigenvector of heisenbergHamiltonianSReMatrixOnMagSector (bipartiteCoupling A) N M at E. This is the spectral witness consumed by tasaki23_toy_sector_groundEnergy_le_of_witness (#3680) to discharge the hμ hypothesis of the witness capstone (#3656) (Issue #3687, PR 22). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/JointPredictedSectorEigenvector.lean) |
| tasaki23_toy_groundState_casimir_eq_predicted | The toy-Hamiltonian ground state is a predicted-total-Casimir witness (for |¬A| ≤ |A|): in the extremal sector M = min(|A|,|¬A|)·N there is a Marshall-positive v > 0 whose embedding magSectorEmbedding (sign · v) is a (Ŝ_tot)²-eigenvector at the predicted value tasaki23PredictedCasimirValue A N. The bipartite toy Hamiltonian’s per-sector Perron–Frobenius ground state (exists_marshallSign_eigenvector_heisenbergHamiltonianSReMatrixOnMagSector) has energy μ ≤ E = predicted − s_A(s_A+1) − s_B(s_B+1) via the predicted-energy sector eigenvector (#3710) and tasaki23_toy_sector_groundEnergy_le_of_witness (#3680); lifting to the full space and feeding μ ≤ E into the witness capstone (#3656) pins its total Casimir to the predicted value. This discharges the single remaining obligation of the sound Perron–Frobenius route (Issue #3658), supplying the hw_cas witness for the overlap pin tasaki23_pf_groundState_casimir_eq_predicted_of_witness. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (eq. 2.5.12) (file Quantum/SpinS/Theorem23ToyWitnessPredicted.lean) |
| tasaki23_pf_groundState_casimir_eq_predicted_base | Base-sector predicted total Casimir (overlap pin with the toy witness) (for |¬A| ≤ |A|): in the base extremal sector M = min(|A|,|¬A|)·N, the Marshall-positive Perron–Frobenius ground state of an arbitrary connected bipartite antiferromagnetic coupling J is a (Ŝ_tot)²-eigenvector at tasaki23PredictedCasimirValue A N. The toy witness (#3711) supplies the predicted-Casimir state in the same sector, and the overlap pin tasaki23_pf_groundState_casimir_eq_predicted_of_witness (Tasaki eq. 2.5.12) transfers the value to the J-ground state. This discharges the hsource_cas hypothesis of the sector-existence chain at the base sector (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (eq. 2.5.12) (file Quantum/SpinS/Theorem23PFBaseCasimir.lean) |
| tasaki23_pf_sector_energy_succ_le_of_casimir, tasaki23_pf_sector_energy_pred_le_of_casimir, tasaki23_pf_sector_energy_eq_of_casimir | Adjacent-sector ground-energy constancy from the predicted total Casimir alone: the adjacent-sector ground-energy bounds and constancy step (Theorem23PFConstancy.lean) restated taking the bare predicted total-Casimir eigen-equation (Ŝ_tot)² Ψ = predicted • Ψ instead of joint bipartiteToyGroundStateSubspacePredicted membership. Inspection of the ladder link (tasaki23_pf_ladder_link_succ/_pred) shows only the total-Casimir eigenvalue (vs. the lowering/raising-kernel value) is consumed; the sublattice components are never used. This matters for the sound route because the ground state of an arbitrary bipartite J carries the predicted total Casimir (overlap pin) but need not be a sublattice-Casimir eigenvector, so it is not in the joint subspace. Hence μ_M = μ_{M+1} for two adjacent Marshall-positive PF ground states sharing the predicted total Casimir (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23PFConstancyCasimir.lean) |
| tasaki23_jointPredicted_lowering_succ | Lowering a joint predicted-Casimir eigenvector to the next sector: a non-zero sector-M (admissible, below the right endpoint) simultaneous eigenvector of (Ŝ_tot)² (at the predicted value), (Ŝ_A)² (at γ_A), (Ŝ_¬A)² (at γ_B) lowers under Ŝ⁻_tot to a non-zero simultaneous eigenvector at the same three eigenvalues. Since Ŝ⁻_tot commutes with all three Casimir operators (totalSpinSSquared_commute_totalSpinSOpMinus, sublatticeSpinSquaredS_commute_totalSpinSOpMinus) the eigenvalues are preserved, and lowering is non-vanishing because the predicted value differs from the sector’s lowering-kernel value. Iterating from the extremal base sector spreads the joint predicted-Casimir line across the whole admissible range — the Casimir-controlled propagation that avoids any lowered Marshall-positivity input (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23JointPredictedLowering.lean) |
| exists_jointPredictedCasimir_embed_base, exists_jointPredictedCasimir_embed_sector | A joint predicted-Casimir eigenvector in every admissible sector (for |¬A| ≤ |A|): in each M ∈ tasaki23GroundStateSectors A N = [min(|A|,|¬A|)·N, max(|A|,|¬A|)·N] there is a non-zero magSectorEmbedding Φ that is a simultaneous eigenvector of (Ŝ_tot)² (at the predicted value), (Ŝ_A)² (at s_A(s_A+1)) and (Ŝ_¬A)² (at s_B(s_B+1)). The base sector M = min(|A|,|¬A|)·N re-derives #3709 in embedded form; the general sector is reached by induction on the distance from the base, lowering with tasaki23_jointPredicted_lowering_succ (#3714) and re-embedding via totalSpinSOpMinus_mulVec_mem_magSubspaceS_of_mem. This is the per-sector predicted-Casimir input the constancy chain (#3713) and overlap pin (#3712) consume, obtained without any lowered Marshall-positivity (“site-sum”) hypothesis (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23JointPredictedSectors.lean) |
| tasaki23_toy_min_energy_arith | Arithmetic core of the toy minimum-energy bound (option (a) toward interior-sector predicted Casimir): for real spin values 0 ≤ a ≤ s_A, 0 ≤ b ≤ s_B ≤ s_A, f(a,b) := |a−b|(|a−b|+1) − a(a+1) − b(b+1) is minimised at the corner (s_A, s_B), i.e. f(s_A, s_B) ≤ f(a, b). Combined with the coupled total-spin lower bound (Ŝ_tot)² ≥ |a−b|(|a−b|+1) on the joint sublattice-Casimir eigenspace W_{a,b} (the Clebsch–Gordan triangle inequality, in progress), this gives Ĥ_toy ≥ bipartiteToyMinEnergyPredicted on each W_{a,b}, hence the global toy minimum-energy bound; see .self-local/tex/3716-tasaki-2-5-toy-min-energy-bound.tex (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23ToyMinEnergyArith.lean) |
| sublatticeSpinSquaredS_re_ge_sublatticeSpinSOp3_mul_succ, sublatticeSpinSquaredS_re_ge_sublatticeSpinSOp3_mul_pred | Sublattice Casimir dominates S³(S³±1) (option (a), Route 5 brick 0): for a simultaneous eigenvector v ≠ 0 of (Ŝ_A)² (eigenvalue γ) and Ŝ_A^(3) (eigenvalue q), (q(q+1)).re ≤ γ.re and (q(q−1)).re ≤ γ.re. From the Cartan identities (Ŝ_A)² = Ŝ_A^∓ Ŝ_A^± + Ŝ_A^(3)(Ŝ_A^(3)±1) and the positive semidefiniteness ⟨v, Ŝ_A^∓ Ŝ_A^± v⟩ = ‖Ŝ_A^± v‖² ≥ 0 (using (Ŝ_A^±)^† = Ŝ_A^∓). This is the magnitude bound (|q| ≤ b on the (Ŝ_A)²=b(b+1) eigenspace) that excludes spurious sublattice weights at the coupled total-spin lower bound’s recurrence boundary; see .self-local/tex/3717-coupled-total-spin-lower-bound.tex (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23SublatticeCasimirSzBound.lean) |
| sublatticeSpinSOpMinus_eq_zero_sublatticeSpinSOp3_re_nonpos | A sublattice lowest weight has non-positive magnetization (option (a), Route 5 brick 1): if v ≠ 0, Ŝ_A^(3) v = q v and Ŝ_A^- v = 0, then q.re ≤ 0. The lowest-weight Casimir relation (Ŝ_A)² = q(q−1) plus the magnitude bound (Ŝ_A)² ≥ q(q+1) (brick 0) force q(q−1) ≥ q(q+1), i.e. q.re ≤ 0. This pins the unique admissible lowest-weight magnetization (q = −b, excluding the spurious root q = b+1) at the recurrence boundary of the coupled total-spin lower bound (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23SublatticeLowestWeightSign.lean) |
| sublatticeMagProjFn_of_mem, sublatticeMagProjFn_of_mem_ne, sublatticeMagProjFn_mulVec_of_commute, sublatticeMagProjFn_sublatticeSpinSquaredS(_complement) | Sublattice magnetization-projection infrastructure (option (a), Route 5 brick 2a): the pointwise sublattice-A magnetization projector sublatticeMagProjFn A M is idempotent on its own subspace, annihilates other subspaces, and commutes with any operator commuting with Ŝ_A^(3) (proved via the magnetization-level decomposition sum_sublatticeMagProjFn_eq). Hence the magnetization component of an (Ŝ_A)²- (resp. (Ŝ_¬A)²-) eigenvector is again a Casimir eigenvector at the same eigenvalue — the Casimir-inheritance needed for the bottom-component extraction of the coupled total-spin lower bound (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23SublatticeMagProjInfra.lean) |
| exists_sublattice_A_lowestWeight_component | Bottom sublattice-A magnetization component is Ŝ_A^--killed (option (a), Route 5 brick 2b): a total lowest-weight w (Ŝ⁻_tot w = 0, total magnetization m, simultaneous sublattice-Casimir eigenvector at α, β) yields a non-zero Ŝ_A^--killed simultaneous weight vector v with Ŝ_A^(3) v = p v, Ŝ_¬A^(3) v = (m−p) v and the inherited Casimir eigenvalues α, β. Obtained as the minimal-A-magnetization nonzero component (max over the magnetization-level projections): projecting Ŝ⁻_tot w = Ŝ_A^- w + Ŝ_¬A^- w = 0 onto the level just below p leaves only Ŝ_A^- v (the Ŝ_¬A^- part preserves A-magnetization and sees only the vanishing lower component). This is the key construction of the coupled total-spin lower bound (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23SublatticeBottomComponent.lean) |
| totalLowestWeight_re_le_complement_sub | One-sided total-magnetization bound (option (a), Route 5 brick 3a): a total lowest weight w in the joint sublattice-Casimir eigenspace with spins a, b ((Ŝ_A)² = a(a+1), (Ŝ_¬A)² = b(b+1)) has m.re ≤ b − a. The bottom-A-component (#brick 2b) is Ŝ_A^--killed at A-weight p, so p ≤ 0 (brick 1) and p(p−1) = a(a+1) (lowest-weight Casimir) force p ≤ −a; the magnitude bound on ¬A (brick 0) gives m − p ≤ b, whence m.re ≤ b + p.re ≤ b − a. Combined with its A ↔ ¬A mirror this yields |m| ≥ |a − b| — the Clebsch–Gordan triangle inequality (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23SublatticeMagBoundOneSide.lean) |
| exists_total_lowestWeight_joint | Total lowest-weight existence with joint Casimir eigenvalues (option (a), Route 5 brick 3b-engine): a non-zero simultaneous eigenvector of (Ŝ_tot)², (Ŝ_A)², (Ŝ_¬A)² reaches, by repeatedly lowering with Ŝ⁻_tot, a non-zero Ŝ⁻_tot-killed vector at the same three eigenvalues (the sublattice Casimirs are preserved since Ŝ⁻_tot commutes with them, #3714). Induction on the magnetization level down to the bottom (where Ŝ⁻_tot annihilates, magEigenvalueS_ne_neg_mMax_sub_one). This is the reduction to the lowest weight for the coupled total-spin lower bound (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23TotalLowestWeightExistence.lean) |
| totalSpinSSquared_re_ge_coupled | Coupled total-spin lower bound (option (a), Route 5 brick 3b — the Clebsch–Gordan triangle inequality): a non-zero (Ŝ_tot)²-eigenvector ψ (eigenvalue γ) in a magnetization level that is also an (Ŝ_A)²- and (Ŝ_¬A)²-eigenvector at a(a+1), b(b+1) (a, b ≥ 0) satisfies |a − b|(|a − b| + 1) ≤ γ.re. Reducing to a total lowest weight w' (#3722) at the same three eigenvalues, the one-sided magnetization bound (#3721) applied to both A and ¬A gives M.re ≤ b−a and M.re ≤ a−b, so |M.re| ≥ |a−b|; the total lowest-weight Casimir relation (Ŝ_tot)² w' = M(M−1) w' then gives γ.re = M.re² − M.re ≥ |a−b|(|a−b|+1). This is the hard representation-theoretic kernel of the toy minimum-energy bound (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23CoupledLowerBound.lean) |
| sublatticeSpinSquaredS_eigenvalue_re_nonneg | The sublattice Casimir is positive semidefinite (option (a) ingredient): any (Ŝ_A)²-eigenvalue γ (non-zero eigenvector) has 0 ≤ γ.re. Since (Ŝ_A)² = Ŝ_A^(1)² + Ŝ_A^(2)² + Ŝ_A^(3)² is a sum of squares of Hermitian operators, ⟨v, (Ŝ_A)² v⟩ = Σ_α ‖Ŝ_A^(α) v‖² ≥ 0. This lets the Casimir eigenvalue be written as a(a+1) with a real sublattice spin a ≥ 0, the form the coupled total-spin lower bound consumes (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23SublatticeCasimirNonneg.lean) |
| toy_joint_eigenvector_energy_re_ge | Toy minimum-energy bound Ĥ_toy ≥ E (option (a) — coupled bound #3723 + arithmetic #3716): a joint (Ŝ_tot)²/(Ŝ_A)²/(Ŝ_¬A)²-eigenvector ψ (eigenvalues γ_tot, γ_A, γ_B) in a magnetization level (with |¬A| ≤ |A|) has toy energy (γ_tot − γ_A − γ_B).re ≥ E = (s_A−s_B)(s_A−s_B+1) − s_A(s_A+1) − s_B(s_B+1). Writing the (non-negative #3724, ≤ s(s+1) #3672) sublattice Casimir eigenvalues as a(a+1), b(b+1) (real spins via the square root), the coupled bound (#3723) gives γ_tot.re ≥ |a−b|(|a−b|+1), hence (γ_tot−γ_A−γ_B).re ≥ |a−b|(|a−b|+1) − a(a+1) − b(b+1) = f(a,b) ≥ f(s_A,s_B) = E (#3716). This is the interior-sector toy minimum-energy bound (pins r_min(M) = E with the predicted-energy witness #3715) (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23ToyMinEnergyBound.lean) |
| tasaki23_toy_min_energy_arith_eq | Strict (equality) arithmetic core (option (a)): if f(a,b) = f(s_A,s_B) on the box 0 ≤ a ≤ s_A, 0 ≤ b ≤ s_B ≤ s_A with s_B > 0, then (a,b) = (s_A,s_B) (the minimiser of f(a,b) = |a−b|(|a−b|+1) − a(a+1) − b(b+1) is the corner). When the toy energy attains its minimum E the toy-minimum-energy chain is tight, so this pins the toy ground state’s sublattice spins to the maximal (s_A,s_B), hence its total Casimir to the predicted value (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23ToyMinEnergyArithEq.lean) |
| toy_joint_eigenvector_totalCasimir_eq_predicted (with tasaki23PredictedCasimirValue_eq_sub) | A minimal-energy joint eigenvector has the predicted total Casimir (option (a), interior-sector culmination): for |¬A| ≤ |A|, s_B > 0, a joint (Ŝ_tot)²/(Ŝ_A)²/(Ŝ_¬A)²-eigenvector ψ (eigenvalues γ_tot, γ_A, γ_B) whose toy energy (γ_tot − γ_A − γ_B).re ≤ E (the predicted minimum) satisfies γ_tot = tasaki23PredictedCasimirValue A N. The toy minimum-energy bound (#3725) forces (γ_tot − γ_A − γ_B).re = E; the coupled bound + equality arithmetic (#3727) force the sublattice spins to the corner (s_A,s_B), whence γ_tot.re = (s_A−s_B)(s_A−s_B+1) = tasaki23PredictedCasimirValue. This is the per-sector toy-ground-state predicted-Casimir witness (any admissible sector), supplying hsource_cas for the overlap pin (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23ToyGSPredictedCasimir.lean) |
| exists_predictedEnergy_sector_eigenvector_of_mem | A predicted-energy real sector eigenvector in every admissible sector (option (a)): generalising #3710 (extremal sector) to each M ∈ tasaki23GroundStateSectors A N via the joint predicted eigenvector at that sector (#3715). The joint eigenvector magSectorEmbedding Φ is a full-space heisenbergHamiltonianS (bipartiteCoupling A)-eigenvector at the predicted toy energy E (Casimir energy formula #3673); restricting to the sector and taking real/imaginary parts (real coupling) gives a non-zero real eigenvector of heisenbergHamiltonianSReMatrixOnMagSector (bipartiteCoupling A) N M at E. This supplies the μ ≤ E witness for the per-sector toy ground-state predicted-Casimir construction (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23PredictedEnergySectorAll.lean) |
| tasaki23_toy_groundState_casimir_eq_predicted_at | The toy ground state has the predicted total Casimir in every admissible sector (option (a), generalising #3711 from the extremal sector): for |¬A| ≤ |A|, s_B > 0, in each M ∈ tasaki23GroundStateSectors A N there is a Marshall-positive v > 0 whose embedding magSectorEmbedding (sign · v) is a (Ŝ_tot)²-eigenvector at tasaki23PredictedCasimirValue A N. The bipartite toy PF ground state is a joint Casimir eigenvector (#3657) with energy μ ≤ E (#3680 via the predicted-energy witness #3729); the minimal-energy joint-eigenvector lemma (#3728) pins its total Casimir to the predicted value. This is the per-sector hsource_cas toy witness for the overlap pin (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23StructuralToyGSPredictedCasimirAt.lean) |
| tasaki23_pf_groundState_casimir_eq_predicted_sector | Per-sector predicted total Casimir for a general bipartite Heisenberg ground state (option (a), generalising the base-sector overlap pin #3712): for |¬A| ≤ |A|, s_B > 0, in every admissible sector M ∈ tasaki23GroundStateSectors A N the Marshall-positive Perron–Frobenius ground state of an arbitrary connected bipartite antiferromagnetic coupling J is a (Ŝ_tot)²-eigenvector at tasaki23PredictedCasimirValue A N. The per-sector toy witness (#3730) supplies the predicted-Casimir state, and the overlap pin (tasaki23_pf_groundState_casimir_eq_predicted_of_witness, Tasaki eq. 2.5.12) transfers the value to the J-ground state. This discharges hsource_cas of the sector-existence chain at every admissible sector (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (eq. 2.5.12) (file Quantum/SpinS/Theorem23StructuralPFSectorCasimir.lean) |
| tasaki23_sector_lift_and_casimir, tasaki23_common_energy_step, tasaki23_common_groundEnergy | Common ground-state energy across every admissible sector (constancy half of Tasaki §2.5 Theorem 2.3) (option (a), TIER 4, PR #3732): for a connected bipartite antiferromagnetic coupling J with |¬A| ≤ |A|, s_B > 0, there is a single energy μ such that in every admissible sector M ∈ tasaki23GroundStateSectors A N the Marshall-positive Perron–Frobenius ground state (from exists_marshallSign_eigenvector_…) has energy μ. Each sector’s ground state is lifted to a full-space H-eigenvector and shown to carry the predicted total Casimir (tasaki23_sector_lift_and_casimir, via #3731); the adjacent-sector Casimir constancy (tasaki23_pf_sector_energy_eq_of_casimir, #3713) then equates neighbouring energies (tasaki23_common_energy_step), and Nat.le_induction along [min·N, max·N] propagates the base-sector energy to the whole interval (tasaki23_common_groundEnergy). Consumes only the predicted total Casimir — never the lowered-Marshall site_sum positivity (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (files Quantum/SpinS/Theorem23StructuralSectorLiftCasimir.lean, Quantum/SpinS/Theorem23StructuralCommonEnergyStep.lean, Quantum/SpinS/Theorem23StructuralCommonGroundEnergy.lean) |
| tasaki23_eigenvalue_ge_common | Global minimality of the common energy — sector min–max engine (option (a), TIER 5, PR #3733): given the common energy μ realised by a Marshall-positive ground state in every admissible sector (hcommon, #3732) and a lower bound hOutside for the non-admissible sectors, every non-zero full-space eigenvector of heisenbergHamiltonianS J N at energy μ' satisfies μ ≤ μ'. Proof: a non-zero eigenvector has a non-zero magnetisation-sector restriction (eq_sum_magSectorEmbedding_magSectorRestriction), which is a sector eigenvector at μ' (…_magSectorRestriction_of_full_eigen); its non-zero real or imaginary part (…_re/_im_of_complex_eigenvec) is a real sector eigenvector; the Collatz–Wielandt per-sector bound (…_eigenvalue_ge_of_marshallPositive) closes the admissible case, hOutside the non-admissible case. The non-admissible bound hOutside is the Lieb–Mattis energy monotonicity E(S_tot) beyond the band, isolated as an explicit hypothesis (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42; Lieb–Mattis, J. Math. Phys. 3 (1962) 749 (file Quantum/SpinS/Theorem23GlobalMinimality.lean) |
| tasaki23_toy_sector_energy_ge_predicted | Toy sector energy lower bound — Lieb–Mattis lower bound for the toy Hamiltonian (option (a), TIER 5, PR #3734): for the bipartite toy Hamiltonian J = bipartiteCoupling A (|¬A| ≤ |A|), in every magnetisation sector M the predicted minimum energy (bipartiteToyMinEnergyPredicted A N).re is below every dressed-sector eigenvalue μM — not just the admissible band. The Marshall-positive Perron–Frobenius sector ground state (exists_marshallSign_eigenvector_…) is a joint Casimir eigenvector (#3657), so the universal toy minimum-energy bound toy_joint_eigenvector_energy_re_ge (#3725) gives its energy ≥ E; the per-sector ground state is below every other sector eigenvalue (tasaki23_toy_sector_groundEnergy_le_of_witness, #3680). This discharges the hOutside hypothesis of the global-minimality engine (#3733) for the toy coupling (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42; Lieb–Mattis, J. Math. Phys. 3 (1962) 749 (file Quantum/SpinS/Theorem23StructuralToySectorLowerBound.lean) |
| totalSpinSOpMinus_mulVec_normSq_eq, totalSpinSOpMinus_mulVec_ne_zero_of_pos_weight, totalSpinSOpPlus_mulVec_ne_zero_of_neg_weight | One total-spin ladder step is non-vanishing on a weight vector (general-J hOutside thread, step 1, PR #3736): from [Ŝ⁺_tot, Ŝ⁻_tot] = 2 Ŝ³_tot (the two Casimir rearrangements) and (Ŝ⁻)† = Ŝ⁺, a weight-w vector Φ (Ŝ³_tot Φ = w Φ) satisfies ‖Ŝ⁻_tot Φ‖² = ‖Ŝ⁺_tot Φ‖² + 2 w ‖Φ‖². Hence Ŝ⁻_tot Φ ≠ 0 when Φ ≠ 0 and w.re > 0, and dually Ŝ⁺_tot Φ ≠ 0 when w.re < 0. This is the SU(2) non-vanishing input for the inward-ladder discharge of the non-admissible-sector lower bound: an eigenvector outside the band can be moved to the band edge by Ŝ∓_tot without annihilation (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42; Lieb–Mattis, J. Math. Phys. 3 (1962) 749 (file Quantum/SpinS/Theorem23TotalLoweringNonvanishing.lean) |
| tasaki23_admissible_eigenvector_ge, raise_iterate_ne_zero, lower_iterate_ne_zero, tasaki23_general_hOutside | General-J non-admissible-sector lower bound via the SU(2) inward ladder (general-J hOutside thread, steps 2–3, PR #3737): discharges, for an ARBITRARY connected bipartite antiferromagnetic coupling J, the hOutside hypothesis of the global-minimality engine (#3733) — every dressed-sector eigenvalue μM in a non-admissible sector M is ≥ the admissible common energy μ. A non-admissible eigenvector is lifted to the full Hilbert space, then moved to the admissible band edge by iterating Ŝ⁺_tot (if M is above the band) or Ŝ⁻_tot (if below): each step commutes with H (energy preserved, heisenbergHamiltonianS_mulVec_totalSpinSOp{Plus,Minus}_mulVec) and is non-zero (#3736, intermediate weights have the right sign), with weight shifts (totalSpinSOp{Plus,Minus}_mulVec_mem_magSubspaceS_of_mem). The landed non-zero eigenvector lies in an admissible sector, where the Collatz–Wielandt per-sector bound tasaki23_admissible_eigenvector_ge (the reused admissible core of the engine) gives μ ≤ μM. This needs only the SU(2) ladder, not reflection positivity (Issue #3542). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42; Lieb–Mattis, J. Math. Phys. 3 (1962) 749 (file Quantum/SpinS/Theorem23GeneralHOutside.lean) |
| tasaki_2_5_theorem_2_3 / tasaki_2_5_theorem_2_3_bipartiteToy | Tasaki §2.5 Theorem 2.3 truly-unconditional capstone for the bipartite toy coupling (#3887 extension chain, Thm23-#3887.12–.21, PR #3891): the canonical tasaki_2_5_theorem_2_3 API is now the structural statement, dropping the vacuous-at-N=1 h_intermediate hypothesis (∀ τ, ∀ x, ∃ z, A z ≠ A x ∧ (τ z).val < N; unsatisfiable when τ ≡ Fin.last 1). The toy capstone tasaki_2_5_theorem_2_3_bipartiteToy proves the conclusion from (1 ≤ N, 1 ≤ |A|, 1 ≤ |¬A|), the genuine physical hypotheses, by chaining structural variants of the entire MLM / sector existence / Casimir / lower-bound stack: complex sector Marshall eigenvector (#3887.12), full-Hilbert lift (#3887.13), four-level Marshall-positive uniqueness chain (#3887.14), Theorem 2.2 bundled full (#3887.15), Theorem 2.3 sector existence wrapper (#3887.16), toy sector energy lower bound (#3887.17), per-sector toy ground state at predicted (#3887.19), final capstone (#3887.21). At spin-1/2 (N=1) this is the first truly-unconditional Tasaki §2.5 Theorem 2.3 closure. The already-h_intermediate-free pieces (tasaki23_eigenvalue_ge_common, tasaki23_toy_sector_groundEnergy_le_of_witness, exists_predictedEnergy_sector_eigenvector_of_mem) are reused directly. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42; Lieb–Mattis, J. Math. Phys. 3 (1962) 749 (file Quantum/SpinS/Theorem23StructuralBipartiteToy.lean) |
| tasaki_2_5_theorem_2_3_of_bipartiteCompletePositive | Tasaki §2.5 Theorem 2.3 truly-unconditional capstone for general bipartite J (PR #3893, Issue #3892): the canonical general-J closure proves tasaki_2_5_theorem_2_3 A N J c for ANY real symmetric non-negative bipartite coupling J positive on the complete bipartite graph at any N ≥ 1, under canonical orientation |¬A| ≤ |A| with s_B > 0. This removes BOTH the toy-coupling restriction of PR #3891 and the vacuous-at-N=1 h_intermediate restriction of the older #3738 capstone. At spin-1/2 (N=1) this is the first truly-unconditional Tasaki §2.5 Theorem 2.3 closure for general bipartite J. Chain: structural sector lift + Casimir (Step 1), structural adjacent-sector common-energy step (Step 2), structural common ground-state energy (Step 3, TIER 4 constancy), capstone (Step 4) combining Step 3 with PR #3891’s marshallLiebMattis_spinS_heisenbergHamiltonianS_groundState_full and the already-h_intermediate-free tasaki23_general_hOutside + tasaki23_eigenvalue_ge_common + heisenbergHamiltonianSReMatrixOnMagSector_eigenvalue_ge_of_marshallPositive. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42; Lieb–Mattis, J. Math. Phys. 3 (1962) 749 (file Quantum/SpinS/Theorem23StructuralGeneralFinal.lean) |
| anisotropicHeisenbergS_unique_groundState_has_zero_magnetization | Tasaki §2.5 Theorem 2.4 partial conclusion: unique GS has zero Ŝ³_tot magnetization (Issue #3739, PR #3896): if the anisotropic Heisenberg ground-state eigenspace has finrank ℂ ≤ 1, every non-zero ground state Φ satisfies Ŝ³_tot Φ = 0. Proof: Φ, Ŝ³_tot Φ, Θ Φ all lie in the GS eigenspace (H commutes with Ŝ³_tot (#3741) and with the reflection Θ (#3745)). From finrank ≤ 1 + Φ ≠ 0 and Module.finrank_le_one_iff, Ŝ³_tot Φ = γ Φ and Θ Φ = δ Φ for some scalars. Θ² = 1 ⟹ δ² = 1 ⟹ δ ≠ 0. Apply the anticommutation Θ Ŝ³_tot = -Ŝ³_tot Θ (#3744) to Φ: get δγ • Φ = -γδ • Φ ⟹ 2δγ • Φ = 0 ⟹ δγ = 0 ⟹ γ = 0 (since δ ≠ 0). This is the second conclusion of Tasaki §2.5 Theorem 2.4 once uniqueness is established (uniqueness itself awaits the deformation argument from the SU(2) point, separate forthcoming work). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/Theorem24ZeroMagnetizationFromUniqueness.lean) |
| anisotropicHeisenbergS_at_SU2_eigenspace_eq_heisenbergHamiltonianS / heisenbergHamiltonianS_unique_groundState_has_zero_magnetization | Tasaki §2.5 Theorem 2.4 SU(2) base case via Theorem 2.3 reduction (Issue #3739, PR #3897): at the SU(2) point (λ=1, D=0), the anisotropic Hamiltonian reduces to the isotropic Heisenberg Hamiltonian (via anisotropicHeisenbergS_one_zero), so every eigenspace coincides. The first lemma gives the direct eigenspace identification; the second specializes PR #3896 to the SU(2) point, giving Ŝ³_tot|Φ⟩=0 for any non-zero GS of the isotropic Heisenberg Hamiltonian under the GS uniqueness hypothesis. Prepares the SU(2) base case for the deformation argument: once uniqueness is established at the SU(2) point (for symmetric |A|=|¬A| via Theorem 2.2 + SU(2) singlet structure, separate forthcoming work), the Ŝ³_tot|Φ⟩=0 conclusion follows immediately. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/Theorem24SU2BaseCase.lean) |
| anisotropicHeisenbergS_apply_eq_zero_of_magSumS_ne | Tasaki §2.5 Theorem 2.4 sector-crossing matrix entries vanish (Issue #3739, PR #3898): the matrix entry anisotropicHeisenbergS J λ D N σ τ = 0 whenever magSumS σ ≠ magSumS τ — the matrix-element form of U(1) invariance [H, Ŝ³_tot] = 0 (#3741). Proof: evaluate H · Ŝ³_tot = Ŝ³_tot · H at (σ, τ); since Ŝ³_tot is diagonal with entries magEigenvalueS, get H σ τ · M_τ = M_σ · H σ τ. When magSumS σ ≠ magSumS τ, Nat-cast injectivity gives magEigenvalueS σ ≠ magEigenvalueS τ, so H σ τ = 0. Key building block for sector-decomposition arguments toward Theorem 2.4 obligation (2.a) uniqueness. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/AnisotropicHeisenbergSectorZero.lean) |
| anisotropicHeisenbergS_magSectorProjection_eigen | Tasaki §2.5 Theorem 2.4 sector projection of eigenvector is eigenvector (Issue #3739, PR #3899): for an eigenvector v of the anisotropic Hamiltonian at μ, the sector projection magSectorEmbedding (magSectorRestriction (M:=M) v) is also an eigenvector at the same μ. Vector-level analog of PR #3898: only same-sector entries survive in the mulVec expansion (cross-sector entries vanish by U(1) invariance). This enables sector-by-sector spectral decomposition of any anisotropic H-eigenvector, key building block toward Theorem 2.4 obligation (2.a) uniqueness via the sector-decomposition + reflection argument. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/AnisotropicSectorProjectionEigenvector.lean) |
| linearIndependent_pair_of_magSubspaceS_distinct | Tasaki §2.5 Theorem 2.4 distinct-sector pair LI (Issue #3739, PR #3900): non-zero vectors in distinct magnetization sectors M₁ ≠ M₂ are linearly independent. Direct consequence of magSubspaceS_disjoint (existing): for a • Φ₁ + b • Φ₂ = 0, get a • Φ₁ ∈ magSubspaceS Λ N M₁ ∩ magSubspaceS Λ N M₂ = ⊥, so a • Φ₁ = 0, giving a = 0 (since Φ₁ ≠ 0), and similarly b = 0. Key technical lemma for the sector-decomposition + reflection argument toward Theorem 2.4 obligation (2.a): non-zero vectors in three pairwise distinct sectors form a 3-LI family, contradicting obligation (1)’s finrank ≤ 2. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/MagSubspaceDistinctLI.lean) |
| linearIndependent_triple_of_magSubspaceS_distinct | Tasaki §2.5 Theorem 2.4 distinct-triple-sector LI (Issue #3739, PR #3901): three non-zero vectors in three pairwise distinct magnetization sectors M₁ ≠ M₂, M₁ ≠ M₃, M₂ ≠ M₃ are linearly independent. Direct application of mathlib’s Module.End.eigenvectors_linearIndependent' to Matrix.toLin' (totalSpinSOp3 Λ N) viewed as a linear endomorphism — magSubspaceS = End.eigenspace of totalSpinSOp3. This is the contradiction lever for the SU(2) symmetric finrank ≤ 1 argument: admissible-sector GS + non-admissible GS + reflected non-admissible GS = 3-LI family contradicting obligation (1) finrank ≤ 2. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/MagSubspaceDistinctTripleLI.lean) |
| anisotropicHeisenbergS_threeLI_of_admis_and_nonadmis | Tasaki §2.5 Theorem 2.4 three-LI from admissible + non-admissible eigenvectors (Issue #3739, PR #3902): for an admissible-sector eigenvector Φ (at Ŝ³_tot = 0) and a non-admissible-sector eigenvector Ψ (at Ŝ³_tot = M' ≠ 0) at the same energy, the family {Φ, Ψ, Θ Ψ} is linearly independent, where Θ Ψ ∈ magSubspaceS Λ N (-M') is the reflected non-admissible eigenvector. Combines PR #3901’s triple-LI with: (i) manyBodyReversalS_mulVec_mem_magSubspaceS_neg (reflection shifts sector M → -M); (ii) Θ² = 1 giving Θ Ψ ≠ 0 from Ψ ≠ 0; (iii) M' ≠ 0 ⟹ 0 ≠ M', 0 ≠ -M', M' ≠ -M' (the latter via 2M' = 0 ⟹ M' = 0). The contradiction lever for the SU(2) symmetric finrank ≤ 1 argument: this 3-LI family combined with obligation (1) finrank ≤ 2 forces no non-admissible-sector eigenstate at the GS energy. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/Theorem24ThreeLIFromNonAdmis.lean) |
| anisotropicHeisenbergS_finrank_le_two_no_admis_plus_nonadmis | Tasaki §2.5 Theorem 2.4 finrank ≤ 2 + admissible + non-admissible → False (Issue #3739, PR #3903): if the anisotropic Hamiltonian eigenspace at μ has finrank ≤ 2 AND contains both an admissible-sector eigenvector Φ (at Ŝ³_tot = 0) and a non-admissible-sector eigenvector Ψ (at Ŝ³_tot = M' ≠ 0), then False. Proof: PR #3902 gives {Φ, Ψ, Θ Ψ} linearly independent; Θ Ψ is also at energy μ via Θ commutes with H (#3745); the 3-LI family lifts to the eigenspace ↥E via LinearIndependent.of_comp E.subtype; LinearIndependent.fintype_card_le_finrank gives 3 ≤ finrank ℂ ↥E, contradicting finrank ≤ 2 via omega. This is the direct contradiction in the SU(2) symmetric finrank ≤ 1 argument. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/Theorem24FinrankLeTwoContradiction.lean) |
| anisotropicHeisenbergS_eigvec_nonadmis_projection_zero | Tasaki §2.5 Theorem 2.4 eigvec non-admissible projection = 0 (Issue #3739, PR #3904): under finrank ≤ 2 at μ + admissible eigvec exists, any eigvec Ψ at μ has zero magSectorEmbedding (magSectorRestriction (M := M) Ψ) for every non-admissible sector index M (with 2M ≠ |Λ|·N). Proof: the projection is an eigvec at μ via PR #3899 and lies in magSubspaceS Λ N M' with M' = |Λ|·N/2 - M ≠ 0 (non-admissible Ŝ³_tot eigenvalue). If non-zero, PR #3903 derives False; hence the projection is 0. Penultimate step toward the SU(2) symmetric finrank ≤ 1: combined with eq_sum_magSectorEmbedding_magSectorRestriction, the eigenspace at μ is contained in the admissible sector. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/Theorem24EigvecNonadmisProjectionZero.lean) |
| anisotropicHeisenbergS_eigvec_in_admis_sector_of_finrank_le_two | Tasaki §2.5 Theorem 2.4 eigvec at μ ∈ admissible sector (Issue #3739, PR #3905): under finrank ≤ 2 at μ + admissible eigvec exists, any eigvec Ψ at μ lies in magSubspaceS Λ N 0 (the Ŝ³_tot = 0 admissible sector). Proof: decompose Ψ via eq_sum_magSectorEmbedding_magSectorRestriction; each summand at non-admissible M is 0 by PR #3904; each summand at admissible M (where 2M = |Λ|·N) lies in magSubspaceS Λ N (|Λ|·N/2 - M) = magSubspaceS Λ N 0; sum of submodule members is in the submodule. Final piece toward the SU(2) symmetric finrank ≤ 1 argument: combined with within-admissible-sector PF finrank = 1, the full Hilbert space finrank at μ is ≤ 1. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/Theorem24EigvecInAdmisSector.lean) |
| anisotropicHeisenbergS_finrank_le_one_from_admis_pf | Tasaki §2.5 Theorem 2.4 finrank ≤ 1 from admis. PF + finrank ≤ 2 (Issue #3739, PR #3906): if the anisotropic Hamiltonian eigenspace at μ has finrank ≤ 2 AND an admissible eigvec exists at μ AND the within-admissible-sector eigenspace at μ has finrank ≤ 1, then the full Hilbert space eigenspace at μ has finrank ≤ 1. Proof: by PR #3905, the eigenspace E is contained in the admissible submodule A, so E ⊓ A = E; the within-admissible hypothesis gives finrank (E ⊓ A) ≤ 1; substitution gives finrank E ≤ 1. The abstract finrank-counting step toward the SU(2) symmetric finrank ≤ 1 capstone, conditional on the within-admissible PF input. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/Theorem24FinrankLeOneFromAdmisPF.lean) |
| heisenbergHamiltonianS_finrank_le_one_at_SU2_conditional | Tasaki §2.5 Theorem 2.4 SU(2) symmetric finrank ≤ 1 (conditional) (Issue #3739, PR #3907): at the SU(2) point (λ=1, D=0), the isotropic Heisenberg Hamiltonian eigenspace at μ has finrank ≤ 1 conditional on (i) finrank ≤ 2 (e.g., from PR #3888 obligation (1) for spin-1/2), (ii) admissible eigvec Φ ≠ 0 at μ, (iii) within-admissible PF input finrank (eigenspace ⊓ admissible) ≤ 1. Proof: transport hypotheses through PR #3897’s eigenspace identification (anisotropic at (1,0) = isotropic Heisenberg) and apply PR #3906. The SU(2) endpoint of the deformation argument toward Theorem 2.4 obligation (2.a): the deformation can now propagate from this μ point. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/Theorem24SU2SymmetricFinrankLeOneConditional.lean) |
| magSectorLinearEquiv | Tasaki §2.5 Theorem 2.4 sector LinearEquiv (Issue #3739, PR #3908): the LinearEquiv between sector-indexed vectors magConfigS Λ N M → ℂ and the corresponding sector subspace magSubspaceS Λ N (|Λ|·N/2 - M) of the full Hilbert space. Forward via magSectorEmbedding (lift), backward via magSectorRestriction (restrict); linearity from magSectorEmbedding_add/magSectorEmbedding_smul; roundtrips via magSectorRestriction_magSectorEmbedding and magSectorEmbedding_magSectorRestriction_of_mem_magSubspaceS. Bridges within-sector-matrix finrank ≤ 1 results to the full Hilbert space ⊓ sector subspace form needed for the SU(2) symmetric finrank ≤ 1 capstone. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/MagSectorLinearEquiv.lean) |
| magSubspaceS_finrank_eq_sector | Tasaki §2.5 Theorem 2.4 sector subspace finrank = sector vector dim (Issue #3739, PR #3909): finrank ℂ ↥(magSubspaceS Λ N (|Λ|·N/2 - M)) = finrank ℂ (magConfigS Λ N M → ℂ). Direct application of PR #3908’s magSectorLinearEquiv via LinearEquiv.finrank_eq. Building block for transferring within-sector PF finrank ≤ 1 to the full Hilbert space ⊓ sector subspace form. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/SectorFinrankTransfer.lean) |
| heisenbergHamiltonianSMatrixOnMagSector_mulVec_magSectorRestriction_of_full_eigen_complex | Tasaki §2.5 Theorem 2.4 sector restriction at ℂ eigenvalue (Issue #3739, PR #3910): ℂ-eigenvalue version of heisenbergHamiltonianSMatrixOnMagSector_mulVec_magSectorRestriction_of_full_eigen. Same proof structure as the ℝ version — the eigenvalue appears only as a scalar multiplier on Ψ, and the matrix-entry sector-zero lemma heisenbergHamiltonianS_apply_eq_zero_of_magSumS_ne does not depend on the eigenvalue. Needed for finrank-level eigenspace transfer (matching End.eigenspace’s ℂ-valued eigenvalues) in the SU(2) symmetric finrank ≤ 1 capstone. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/SectorRestrictionComplexEigval.lean) |
| heisenbergHamiltonianS_mulVec_magSectorEmbedding_complex | Tasaki §2.5 Theorem 2.4 sector embedding at ℂ eigenvalue (Issue #3739, PR #3911): ℂ-eigenvalue version of heisenbergHamiltonianS_mulVec_magSectorEmbedding. Together with PR #3910 (restriction direction), provides the two-sided ℂ-eigenvalue correspondence between the sector matrix and the full Hilbert space. Same proof structure as the ℝ version — eigenvalue appears only as a scalar multiplier; sector-zero matrix-entry lemma is eigenvalue-independent. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/SectorEmbeddingComplexEigval.lean) |
| heisenbergHamiltonianS_sector_matrix_eigenspace_finrank_eq | Tasaki §2.5 Theorem 2.4 eigenspace finrank equality between sector matrix and full Hilbert ⊓ sector (Issue #3739, PR #3912): finrank ℂ ↥(End.eigenspace (Matrix.toLin' (heisenbergHamiltonianSMatrixOnMagSector J N M)) μ) = finrank ℂ ↥(End.eigenspace (Matrix.toLin' (heisenbergHamiltonianS J N)) μ ⊓ magSubspaceS Λ N (|Λ|·N/2 - M)). Build a LinearEquiv between the two eigenspaces using magSectorEmbedding (forward, with full-eigvec property via PR #3911) and magSectorRestriction (backward, with sector-eigvec property via PR #3910). Round-trips via magSectorRestriction_magSectorEmbedding and magSectorEmbedding_magSectorRestriction_of_mem_magSubspaceS. The within-admissible PF input transfer needed for the SU(2) symmetric finrank ≤ 1 capstone. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/EigenspaceSectorFinrankEq.lean) |
| heisenbergHamiltonianS_eigenspace_inf_magSubspaceS_finrank_le_one_of_sector | Tasaki §2.5 Theorem 2.4 sector finrank ≤ 1 ⟹ full Hilbert ⊓ sector finrank ≤ 1 (Issue #3739, PR #3913): direct application of PR #3912’s finrank equality — if the sector matrix’s μ-eigenspace has finrank ≤ 1, then the full Hilbert space μ-eigenspace ⊓ the sector subspace also has finrank ≤ 1. This is the within-admissible Perron–Frobenius input transfer that connects the existing Theorem 2.3 chain’s sector-matrix PF uniqueness to the abstract finrank ≤ 1 machinery (PR #3906/#3907) for the SU(2) symmetric finrank ≤ 1 capstone. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/EigenspaceFinrankLeOneTransfer.lean) |
| heisenbergHamiltonianS_finrank_le_one_at_SU2_from_sector_pf | Tasaki §2.5 Theorem 2.4 SU(2) symmetric finrank ≤ 1 from sector matrix PF (Issue #3739, PR #3915): combines PR #3907 (SU(2) symmetric finrank ≤ 1 conditional on within-admissible PF) and PR #3913 (sector matrix finrank ≤ 1 transfer) to express the SU(2) symmetric finrank ≤ 1 conclusion with the within-admissible PF input at the sector matrix level — matching the output form of the existing Theorem 2.3 chain’s PF analysis. Conditional on: obligation (1) finrank ≤ 2, admissible eigvec Φ ≠ 0 at μ, sector index M with 2M = |Λ|·N (the symmetric |A|=|¬A| admissible sector value), and within-admissible sector-matrix PF finrank ≤ 1. The bridge between Theorem 2.3 chain’s PF infrastructure and the SU(2) symmetric capstone. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/Theorem24SU2SymmetricFinrankLeOneFromSectorPF.lean) |
| heisenbergHamiltonianS_finrank_le_one_at_SU2_symmetric_card_eq | Tasaki §2.5 Theorem 2.4 SU(2) symmetric finrank ≤ 1 via |A|=|¬A| card equality (Issue #3739, PR #3916): packaging of PR #3915 that replaces the abstract 2M = |Λ|·N hypothesis with the natural symmetric sublattice card equality |A| = |¬A|. Sector index M := |A|·N automatically satisfies the constraint via tasaki23_card_filter_A_add_card_notA. The same conditional hypotheses (obligation (1) finrank ≤ 2, admissible eigvec, within-admissible sector-matrix PF) apply. This is the natural physical statement form of the SU(2) symmetric capstone. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43-44 (file Quantum/SpinS/Theorem24SU2SymmetricFinrankLeOneCardEq.lean) |
| spinSDotXXZ, singleIonAnisotropyS, anisotropicHeisenbergS | Anisotropic (XXZ + single-ion) antiferromagnetic Hamiltonian (Tasaki (2.5.14), Theorem 2.4 foundation, Issue #3739, PR #3740): Ĥ = Σ_{x,y} J_{x,y}(Ŝ_x⁽¹⁾Ŝ_y⁽¹⁾ + Ŝ_x⁽²⁾Ŝ_y⁽²⁾ + λ Ŝ_x⁽³⁾Ŝ_y⁽³⁾) + D Σ_x (Ŝ_x⁽³⁾)² with Ising anisotropy λ and crystal-field D. Built from onSiteS x (spinSOp{1,2,3} N). Hermitian for real J, λ, D (anisotropicHeisenbergS_isHermitian_of_real); reduces to the isotropic Heisenberg Hamiltonian at λ = 1, D = 0 (anisotropicHeisenbergS_one_zero, in Quantum/SpinS/AnisotropicHeisenbergReduction.lean — split out so the core defs do not import the heavy Heisenberg module). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (eq. 2.5.14) (file Quantum/SpinS/AnisotropicHeisenberg.lean) |
| anisotropicHeisenbergS_commute_totalSpinSOp3, anisotropicHeisenbergS_mulVec_mem_magSubspaceS_of_mem | U(1) invariance of the anisotropic Hamiltonian (Tasaki §2.5 Theorem 2.4, Issue #3739, PR #3741): the anisotropic XXZ + single-ion Hamiltonian commutes with Ŝ³_tot (it is U(1)- but not SU(2)-invariant) and therefore preserves each magnetization sector magSubspaceS Λ N M. Each site Ŝ³ commutes with Ŝ³_tot (onSiteS_spinSOp3_commute_totalSpinSOp3), so the longitudinal Ŝ³Ŝ³ and single-ion terms do; the transverse Ŝ¹Ŝ¹+Ŝ²Ŝ² part commutes via spinSDotXXZ = spinSDot + (λ−1)Ŝ³Ŝ³ and spinSDot_commutator_totalSpinSOp3. This is the symmetry underlying the sector-by-sector Mattis–Nishimori argument. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (file Quantum/SpinS/AnisotropicHeisenbergU1.lean) |
| spinSOp1_mul_spinSOp1_add_spinSOp2_mul_spinSOp2, spinSOp1_mul_spinSOp1_sub_spinSOp2_mul_spinSOp2 | Transverse spin operators in ladder form (Tasaki §2.5 Theorem 2.4, eq. 2.5.16, Issue #3739, PR #3742): Ŝ¹Ŝ¹ + Ŝ²Ŝ² = ½(Ŝ⁺Ŝ⁻ + Ŝ⁻Ŝ⁺) (longitudinal-preserving) and Ŝ¹Ŝ¹ − Ŝ²Ŝ² = ½(Ŝ⁺Ŝ⁺ + Ŝ⁻Ŝ⁻) (longitudinal-flipping by ±2), via Ŝ¹ = (Ŝ⁺+Ŝ⁻)/2, Ŝ² = (Ŝ⁺−Ŝ⁻)/(2i) and (1/(2i))² = −1/4. These are the single-site identities behind Tasaki’s rewriting (2.5.16) of the anisotropic XXZ Hamiltonian into ladder form for the Marshall-sign analysis. Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (eq. 2.5.16) (file Quantum/SpinS/SpinSTransverseLadder.lean) |
| onSiteS_spinSOp1_mul_add_onSiteS_spinSOp2_mul, onSiteS_spinSOp1_mul_sub_onSiteS_spinSOp2_mul | Two-site transverse bond in ladder form (Tasaki §2.5 Theorem 2.4, eq. 2.5.16, Issue #3739, PR #3747): the bond-level (cross-site x ≠ y) version of #3742 — Ŝ¹_x Ŝ¹_y + Ŝ²_x Ŝ²_y = ½(Ŝ⁺_x Ŝ⁻_y + Ŝ⁻_x Ŝ⁺_y) (magnetization-preserving) and Ŝ¹_x Ŝ¹_y − Ŝ²_x Ŝ²_y = ½(Ŝ⁺_x Ŝ⁺_y + Ŝ⁻_x Ŝ⁻_y) (magnetization-flipping by ±2), via onSiteS distributing over Ŝ¹ = (Ŝ⁺+Ŝ⁻)/2, Ŝ² = (Ŝ⁺−Ŝ⁻)/(2i). These give the (1+λ)/4 (Ŝ⁺Ŝ⁻+Ŝ⁻Ŝ⁺) + (1−λ)/4 (Ŝ⁺Ŝ⁺+Ŝ⁻Ŝ⁻) ladder split of the XXZ bond in (2.5.16). Tasaki, Springer 2020, §2.5 Theorem 2.4, p. 43 (eq. 2.5.16) (file Quantum/SpinS/TwoSiteTransverseLadder.lean) |
← Perron-Frobenius theorem (Math/PerronFrobenius.lean, Math/PerronFrobeniusPrimitive.lean, Math/CollatzWielandt.lean, Math/PerronFrobeniusMain.lean) · Catalogue · Spin-S Marshall–Lieb–Mattis on the magnetization sector (Tasaki §2.5 Theorem 2.2 generic S, sector form) →