S saturated ferromagnetic state (Tasaki §2.4 generalised) (part 2 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
| Lean name | Statement |
|—|—|
| twoSpinPlusMinus_ladder_signed_entry_re_pos_of_off_two_site_raise_lower / exists_twoSpinPlusMinus_ladder_signed_entry_re_pos_of_bipartite_ne_balanced_sector / twoSpinCorrelationS_bipartite_signed_re_pos_of_marshall_balanced_sector_cross_eigenphase | Problem 2.5.d balanced-sector ladder witness: supplies the strict sector-local S_x^+ S_y^- matrix-entry witness required by PR #4076 at the balanced sector M0 = |A| * N. The witness starts from the complement Néel configuration, updates the two cross-sublattice sites touched by the ladder operator, and uses magSumS_configUpdateTwo_eq plus magSumS_neelConfigOfS_complement to keep both configurations in M0. The resulting wrapper removes the explicit strict-entry hypothesis from the sector-supported eigenspace-phase theorem at the balanced sector. 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 #4077, files Quantum/SpinS/Problem25dBalancedSectorWitnessCore.lean for the signed ladder entries and balanced-sector witness + Quantum/SpinS/Problem25dBalancedSectorWitness.lean for the balanced-sector dot-product wrapper, split for build speed) |
| phase_unit_of_unitary_mulVec_eq_smul_of_ne_zero / exists_phase_unit_of_finrank_eigenspace_le_one_of_unitary_commute_of_ne_zero / twoSpinCorrelationS_bipartite_signed_re_pos_of_tasaki23_balanced_pf_cross | Problem 2.5.d balanced Perron-Frobenius endpoint: extracts the balanced sector PF vector from the Theorem 2.3 common-energy data, rewrites the existing real-sign embedding into the sector-supported Marshall form using marshallSignS_eq_ofReal_re, and derives the axis-swap / z-rotation unit-modulus phases without normalizing the vector. The endpoint returns the common Hermitian minimum, the strictly positive balanced coefficients, the non-zero embedded eigenvector, the full eigenspace finrank ≤ 1 input from the SU(2) endpoint, and the signed cross-sublattice two-spin correlation positivity for that concrete PF vector. 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 #4078, files Quantum/SpinS/Problem25dBalancedPFEndpointCore.lean for the non-normalized phase bridge + Quantum/SpinS/Problem25dBalancedPFEndpoint.lean for the balanced PF endpoint correlation positivity, split for build speed) |
| twoSpinCorrelationS_sign_cases_of_tasaki23_balanced_pf_cross | Problem 2.5.d balanced Perron-Frobenius sign cases: applies the final bipartite-gauge sign conversion to the concrete balanced PF endpoint from PR #4078. The wrapper preserves the Hermitian minimum, strictly positive balanced coefficients, non-zero embedded eigenvector, and full eigenspace finrank ≤ 1 package, while replacing the signed-positivity conclusion by the four Boolean same-sublattice positive / cross-sublattice negative sign cases for the original two-spin correlation. 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 #4079, file Quantum/SpinS/Problem25dBalancedPFSignCases.lean) |
| twoSpinCorrelationS_re_neg_of_tasaki23_balanced_pf_cross | Problem 2.5.d balanced Perron-Frobenius cross sign: extracts the concrete non-vacuous cross-sublattice conclusion from PR #4079. Under A x ≠ A y, the Boolean sign cases collapse to the original two-spin correlation inequality (twoSpinCorrelationS x y Φ).re < 0 for the same balanced PF vector, while preserving the Hermitian minimum, positive coefficients, non-zero eigenvector, and finrank ≤ 1 package. 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 #4080, file Quantum/SpinS/Problem25dBalancedPFCrossSign.lean) |
| spinSOp{Plus,Minus,1,2,3}_one_eq_spinHalfOp{Plus,Minus,1,2,3} | spin-S ↔ spin-1/2 bridge at N = 1: spinSOp{Plus, Minus, 1, 2, 3} 1 = spinHalfOp{Plus, Minus, 1, 2, 3} (each is the corresponding half-Pauli matrix) (PRs #922 + #923, file Quantum/SpinS/SpinHalfSpecialization.lean) |
| onSiteS_spinSOp3_mulVec_allAlignedStateS / allAlignedStateS_expectation_onSiteS_spinSOp3 / _sq / onSiteS_spinSOp3_sq_mulVec_allAlignedStateS | single-site Ŝ^(3)_x and (Ŝ^(3)_x)² on |c..c⟩: Ŝ^(3)_x · |c..c⟩ = (N/2 − c.val) · |c..c⟩ and expectation of (Ŝ^(3)_x)² is (N/2 − c.val)² (PR #925, file Quantum/SpinS/SingleSiteZExpectation.lean) |
| allAlignedStateS_expectation_onSiteS_spinSOp1_sq_add_spinSOp2_sq | xy-plane Casimir expectation: ⟨((Ŝ^(1)_x)² + (Ŝ^(2)_x)²) · |c..c⟩⟩ = N(N+2)/4 − (N/2 − c.val)². From #920 minus #925; for c=0 gives S/2 (PR #926, file Quantum/SpinS/SingleSiteXYExpectation.lean) |
| basisVecS_expectation_onSiteS_spinSOp1 / _spinSOp2 / allAlignedStateS_expectation_onSiteS_spinSOp1 / _spinSOp2 | transverse mean is zero: ⟨basisVecS σ, Ŝ^(α)_x · basisVecS σ⟩ = 0 for α = 1, 2 (transverse operators are purely off-diagonal). Specialised to |c..c⟩ (PR #927, file Quantum/SpinS/SingleSiteTransverseMeanZero.lean) |
| spinSDot_mulVec_allAlignedStateS_zero_of_ne | per-pair eigenvalue: for x ≠ y, Ŝ_x · Ŝ_y · |σ_⊤⟩ = (N²/4) · |σ_⊤⟩. Proof via spinSDot_eq_plus_minus: ladder annihilations + (3)(3) → (N/2)² (PR #939, file Quantum/SpinS/SpinSDotAllAlignedZero.lean) |
| spinSDot_mulVec_allAlignedStateS_last_of_ne | symmetric raising-side per-pair eigenvalue on |σ_⊥⟩ (PR #940, file Quantum/SpinS/SpinSDotAllAlignedLast.lean) |
| allAlignedStateS_zero_expectation_heisenbergHamiltonianS / _last_expectation_heisenbergHamiltonianS | Heisenberg expectation on saturated states: ⟨|σ_⊤⟩, H · |σ_⊤⟩⟩ = saturatedFerromagnetEigenvalueS J N; ⟨|σ_⊥⟩, H · |σ_⊥⟩⟩ = H(σ_⊥, σ_⊥) (PR #943, file Quantum/SpinS/SaturatedHeisenbergExpectation.lean) |
| heisenbergHamiltonianS_diag_allAlignedConfigS_last_eq_zero | H(σ_⊥, σ_⊥) = saturatedFerromagnetEigenvalueS J N: both extremal H-diagonals equal (via #875/#876 same explicit formula + uniqueness on non-zero eigenvectors) (PR #946, file Quantum/SpinS/SaturatedHeisenbergSymmetric.lean) |
| saturatedFerromagnetEigenvalueS_explicit / saturatedFerromagnetEigenvalueS_im_zero / saturatedFerromagnetEigenvalueS_exists_real | explicit form and realness: saturatedFerromagnetEigenvalueS J N = ∑_x ∑_y J(x,y) · (if x = y then N(N+2)/4 else (N/2)²), and real couplings make this saturated energy a real scalar. (PR #951 and Tasaki §2.5 Theorem 2.3 follow-up, file Quantum/SpinS/SaturatedEigenvalueExplicit.lean) |
| allAlignedConfigS_injective / allAlignedStateS_ne_of_ne | distinct constants give distinct configurations and distinct states for [Nonempty V] (PR #956, file Quantum/SpinS/AllAlignedStateDistinct.lean) |
| allAlignedStateS_inner_of_ne | all-aligned states at distinct constants are orthogonal (PR #960, file Quantum/SpinS/AllAlignedStateOrthogonal.lean) |
| allAlignedStateS_mem_magSubspaceS | |c..c⟩ ∈ magSubspaceS V N (|V|·N/2 − |V|·c.val) for any c (PR #962, file Quantum/SpinS/AllAlignedStateMagSubspace.lean) |
References: H. Tasaki, Physics and Mathematics of Quantum Many-Body Systems, Springer 2020, §2.4 (pp. 30–37, spin-1/2 case).
← Spin-S saturated ferromagnetic state (Tasaki §2.4 generalised) · Catalogue · Single-mode fermion (P2 skeleton) →