S Marshall–Lieb–Mattis on the magnetization sector (Tasaki §2.5 Theorem 2.2 generic S, sector form) (part 4 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
| Lean name | Statement |
|—|—|
| marshallDiagonalOnMagSector / marshallDiagonalOnMagSector_mul_self / dressedHeisenbergSReMatrixOnMagSector_map_eq_marshall_conj_heisenberg / heisenbergHamiltonianSMatrixOnMagSector_finrank_le_one_of_marshall_positive / tasaki23_balanced_sector_matrix_finrank_le_one_of_common_min / exists_t23_commonE_and_heisHamS_fullEig_finrank_le_one_of_casLadder_t23_pf / spinHalf_anisotropicHeisenbergS_obligation_2_of_MLM_casimir_ladder_t23_pf | Balanced-sector PF simplicity from the Theorem 2.3 witness (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4027): builds the sector Marshall diagonal similarity, derives real shifted-dressed PF geometric simplicity from a Marshall-positive Theorem 2.3 sector witness, transfers it through shift, real-to-complex, and Marshall-conjugation bridges to the bare complex sector matrix, and feeds that bound into the MLM/Casimir SU(2) endpoint and spin-1/2 obligation wrapper. This removes the explicit balanced-sector PF simplicity callback from the current spin-half obligation boundary; the remaining inputs are the structural Theorem 2.3 predicate, coupling/diagonal strictness hypotheses, balanced-cardinality arithmetic, and the deformation-path hypotheses. Tasaki, Springer 2020, §2.5 Theorems 2.3 and 2.4, pp. 42–44; Lieb-Mattis, J. Math. Phys. 3 (1962), 749 (files Quantum/SpinS/Theorem24SectorPFFromTheorem23.lean, Quantum/SpinS/Theorem24SU2GlobalUniquenessFromMLM.lean, Quantum/SpinS/AnisotropicHeisenbergSpinHalfObligation2FromMLM.lean) |
| spinHalf_anisotropicHeisenbergS_obligation_2_strict_gap_of_MLM_casimir_ladder_t23_pf | Spin-1/2 obligation (2) strict-gap form from Theorem 2.3 PF (Tasaki §2.5 Theorem 2.4 obligation (2), PR #4028): repackages the PR #4027 contradiction theorem into the public strict-gap statement E_balanced(λ',D') < E_M(λ',D') for every non-balanced sector in the strict deformation region. The proof is order-theoretic: if the strict gap failed, E_M(λ',D') ≤ E_balanced(λ',D') is exactly the violation consumed by spinHalf_anisotropicHeisenbergS_obligation_2_of_MLM_casimir_ladder_t23_pf, so the contradiction theorem rules it out. No new mathematical callback is introduced; the inputs remain Theorem 2.3, coupling/diagonal strictness, balanced-cardinality arithmetic, and the deformation-path hypotheses. Tasaki, Springer 2020, §2.5 Theorems 2.3 and 2.4, pp. 42–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinHalfObligation2FromMLM.lean) |
| spinHalf_anisotropicHeisenbergS_strict_gap_all_M_of_MLM_casimir_ladder_t23_pf / spinHalf_anisotropicHeisenbergS_balanced_eq_full_of_MLM_casimir_ladder_t23_pf | Spin-1/2 balanced target sector is the full ground sector from Theorem 2.3 PF (Tasaki §2.5 Theorem 2.4, PR #4029): packages PR #4028’s per-sector strict gap into a uniform statement over every non-empty M ≠ M_balanced, then applies hermitianMinEigenvalue_balanced_eq_full_of_strict_gap at the target point (λ',D'). The result is the consumer ground-energy equality E_balanced(λ',D') = λ_min(Ĥ(λ',D')), with no new mathematical callback beyond the Theorem 2.3/PF strict-gap inputs. This is the next bridge toward the final ground-eigenspace uniqueness plus Ŝ³_tot zero statement. Tasaki, Springer 2020, §2.5 Theorems 2.3 and 2.4, pp. 42–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinHalfBalancedGSFromMLM.lean) |
| anisotropicHeisenbergS_sector_matrix_eigenspace_finrank_eq / dressedAnisotropicHeisenbergSReMatrixOnMagSector / shiftedDressedAnisotropicHeisenbergSReMatrixOnMagSector / isIrreducible_shiftedDressedAnisotropicHeisenbergSReMatrixOnMagSector / anisotropicHeisenbergS_magSector_submatrix_finrank_le_one_at_hermitianMinEigenvalue / spinHalf_anisotropicHeisenbergS_balanced_sector_pf_at_target / spinHalf_anisotropicHeisenbergS_target_finrank_le_one_of_MLM_casimir_ladder_t23_pf / spinHalf_aHeisS_target_gState_zeroMag_of_MLM_casLadder_t23_pf | Spin-1/2 target uniqueness with target balanced-sector PF discharged (Tasaki §2.5 Theorem 2.4, Issue #3739): PR #4030 added the anisotropic sector-matrix/full-intersection eigenspace finrank transfer and the conditional target uniqueness wrappers. The new anisotropic sector PF layer defines real and Marshall-dressed sector matrices, proves shifted non-negativity and irreducibility from the spin-(S) bipartite reachability theorem, applies Perron–Frobenius plus Collatz–Wielandt at the shifted matrix, and transfers the resulting geometric simplicity through the strict shift, real-to-complex bridge, and Marshall similarity. The spin-1/2 target wrapper chooses a diagonal-dominating shift and supplies the balanced-sector PF bound directly, so the public target uniqueness and zero-magnetization wrappers no longer require an explicit h_balanced_sector_pf hypothesis. Tasaki, Springer 2020, §2.5 Theorems 2.3 and 2.4, pp. 42–44 (files Quantum/SpinS/AnisotropicEigenspaceSectorFinrankEq.lean, Quantum/SpinS/DressedAnisotropicMatrixOnMagSector.lean, Quantum/SpinS/AnisotropicSectorPFAtMin.lean, Quantum/SpinS/AnisotropicHeisenbergSpinHalfTargetUniquenessFromBalancedPF.lean) |
| singleIonStepS_spinHalf_false / spinHalf_anisotropicHeisenbergS_eigenspace_finrank_le_two_at_global_min_D_nonneg / spinHalf_anisotropicHeisenbergS_obligation_2_of_MLM_casimir_ladder_t23_pf_D_nonneg / spinHalf_anisotropicHeisenbergS_balanced_eq_full_of_MLM_casimir_ladder_t23_pf_D_nonneg / spinHalf_anisotropicHeisenbergS_target_finrank_le_one_of_MLM_casimir_ladder_t23_pf_D_nonneg / spinHalf_aHeisS_target_gState_zeroMag_of_MLM_casLadder_t23_pf_D_nonneg | Spin-1/2 case-(i) D ≥ 0 boundary extension (Tasaki §2.5 Theorem 2.4, Issue #412): specializes the parity-block Perron–Frobenius route to spin 1/2, where the single-ion ±2 parity step is impossible. The raise/lower and parity-bond positivity inputs only require D.re ≥ 0, so the parity-block irreducibility, global finrank ℂ ≤ 2, deformation contradiction, balanced-sector ground-energy equality, and final target uniqueness/zero-magnetization wrappers extend from D > 0 to D ≥ 0 while retaining -1 < λ < 1. The strict parity-block route does not cover the λ = 1 edge; the following row records the separate scalar-shift boundary. Case (ii) now has conditional, strict-gap, and no-full-finrank bridges, with the strict-gap derivation still explicit; the general spin-S D >= 0 endpoint is recorded in the general boundary row above. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (files Quantum/SpinS/AnisotropicHeisenbergSpinHalfDNonnegBoundary.lean + the parity-block PF core Quantum/SpinS/AnisotropicHeisenbergSpinHalfDNonnegBoundaryCore.lean) |
| spinSOp3_one_sq_eq_quarter_smul_one / singleIonAnisotropyS_spinHalf_eq_scalar / anisotropicHeisenbergS_one_D_spinHalf_eq_heisenberg_add_scalar / eigenspace_add_smul_one_eq / hermitianMinEigenvalue_add_smul_one / spinHalf_anisotropicHeisenbergS_lambda_one_finrank_le_one_of_MLM_casimir_ladder_t23_pf / spinHalf_aHeisS_lam1_gState_zeroMag_of_MLM_casLadder_t23_pf | Spin-1/2 case-(i) λ = 1 scalar-shift boundary (Tasaki §2.5 Theorem 2.4, Issue #412): at spin 1/2, (S^3)^2 = (1/4)I, hence singleIonAnisotropyS D 1 = (D |Λ| / 4) • 1 and anisotropicHeisenbergS J 1 D 1 is the Heisenberg Hamiltonian plus a scalar shift. Generic scalar-shift eigenspace and Hermitian-minimum lemmas transfer the Theorem 2.3/MLM SU(2) full-ground uniqueness to the anisotropic λ = 1 endpoint, and the existing uniqueness-to-zero-magnetization theorem supplies Ŝ³_tot Φ = 0. This bypasses the strict parity-bond PF route, whose coefficient (1 - λ) / 4 vanishes at λ = 1. Tasaki, Springer 2020, §2.5 Theorem 2.4, pp. 43–44 (file Quantum/SpinS/AnisotropicHeisenbergSpinHalfLambdaOneBoundary.lean) |
| raiseLowerReachableSMagSector_bipartiteCompleteGraph_structural / exists_matrixPow_pos_of_magConfigS_bipartite_structural / exists_matrixPow_pos_length_of_magConfigS_bipartite_structural / isIrreducible_shiftedDressedSReMatrixOnMagSector_structural | (Thm23-#3887.1) Theorem 2.3 chain structural reachability + sector irreducibility (no h_intermediate) (Tasaki §2.5 Theorem 2.3, PR #3890): extension of #3887 fix to Theorem 2.3 dressed-Heisenberg chain. Drops h_intermediate; requires hA_ne + hB_ne + 1 ≤ N. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23StructuralReach.lean) |
| tasaki23_shiftedDressed_sector_eigenvec_proportional_structural / tasaki23_heis_sector_eigenvec_proportional_of_marshallPositive_structural | (Thm23-#3887.2+.3) Theorem 2.3 sector eigenvec proportionality structural (no h_intermediate) (Tasaki §2.5 Theorem 2.3, PR #3890): structural variants using (Thm23-#3887.1). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23StructuralCasimirEigenvec.lean) |
| tasaki23_pf_groundState_commuting_eigenvector_structural / tasaki23_toy_groundState_joint_casimir_eigenvector_structural | (Thm23-#3887.4+.5) Theorem 2.3 PF GS commuting + toy joint Casimir eigenvector structural (no h_intermediate) (Tasaki §2.5 Theorem 2.3, PR #3890): full chain reconstructed without h_intermediate up to the joint Casimir eigenvector for the toy Hamiltonian. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23StructuralPFJointCasimir.lean) |
| totalSpinSSquared_eigenvalue_re_le_sMax (with exists_highestWeight_eigenvector, totalSpinSSquared_highestWeight_eigenvalue_re_le) | Total-Casimir spectral max bound (Ŝ_tot)²-eigenvalue ≤ s_max(s_max+1), s_max = |V|·N/2. Highest-weight argument: a non-zero (Ŝ_tot)²-eigenvector at γ has a non-zero weight component (totalSpinSSquared_eigenvec_exists_weight_component); raising it with Ŝ⁺_tot terminates (induction on the depth k below s_max; the magSubspace above s_max is ⊥ via magEigenvalueS_ne_mMax_add_one), giving a highest-weight vector with Ŝ⁺_tot w' = 0; then γ = M(M+1) (tasaki23_totalSpinSSquared_mulVec_of_totalSpinSOpPlus_eq_zero_of_mem_magSubspaceS) with M an achievable magnetization (|M| ≤ s_max, PR 1), so γ.re = M.re(M.re+1) ≤ s_max(s_max+1). Issue #3658 PR 3 — the spectral facts underlying the toy variational minimisation. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/CasimirSpectralBound.lean) |
| totalSpinSSquared_eigenvec_exists_weight_component | Weight-component extraction for total-Casimir eigenvectors: since (Ŝ_tot)² commutes with the magnetization projection magProjFn, a non-zero (Ŝ_tot)²-eigenvector at γ has a non-zero weight component magProjFn M v (M = |V|·N/2 − k) that is again a (Ŝ_tot)²-eigenvector at γ and lies in magSubspaceS V N M. Reduces the Casimir spectral max bound to weight eigenvectors. Scaffold (Issue #3658, PR 3a). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/CasimirWeightComponent.lean) |
| sublatticeSpinSOp3_mulVec_basisVecS / sublatticeSpinSOp3_eigenvalue_re_abs_le_sA | Sublattice magnetization eigenvalue bound |M_z^A| ≤ s_A = |A|·N/2. Ŝ_A^(3) acts diagonally on |σ⟩ with eigenvalue ∑_{x∈A}(N/2 − σ_x); each term ∈ [−N/2, N/2], so the sum over |A| sites is bounded by s_A. Scaffold (Issue #3658, PR 2) for the highest-weight argument toward the sublattice Casimir (Ŝ_A)² spectral max bound. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeSzBound.lean) |
| magEigenvalueS_re_le_sMax / neg_sMax_le_magEigenvalueS_re / magEigenvalueS_re_sq_le_sMax_sq | Magnetization eigenvalue bounds |M_z| ≤ s_max (and M_z² ≤ s_max²), where M_z = (magEigenvalueS σ).re = |Λ|·N/2 − magSumS σ and s_max = |Λ|·N/2. From 0 ≤ magSumS σ ≤ |Λ|·N. Scaffold (Issue #3658, PR 1) for the highest-weight argument toward the total-Casimir spectral max bound — the final obligation of the sound §2.5 Theorem 2.3 route. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/MagEigenvalueBound.lean) |
| tasaki23_pf_groundState_commuting_eigenvector / tasaki23_toy_groundState_joint_casimir_eigenvector | The toy-Hamiltonian ground state is a simultaneous Casimir eigenvector. The first generalises tasaki23_pf_groundState_casimir_eigenvector to any operator B commuting with Ĥ and with Ŝ_tot^(3): the per-sector Marshall-positive ground state is a B-eigenvector (same one-dimensionality argument). Instantiated at the toy Hamiltonian Ĥ_toy = heisenbergHamiltonianS (bipartiteCoupling A) for B = (Ŝ_tot)², (Ŝ_A)², (Ŝ_¬A)² — all of which commute with Ĥ_toy (it is their linear combination, heisenbergToyHamiltonianS_commute_{totalSpinSSquared,sublatticeSpinSquaredS,_complement}), unlike with the general Heisenberg Ĥ — the toy ground state is a joint eigenvector of all three. Pinning the three eigenvalues to the predicted (max sublattice, min total) values is the remaining variational obligation. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23StructuralPFJointCasimir.lean) |
| tasaki23_pf_groundState_casimir_eq_predicted_of_witness (with isHermitian_eigenvalue_star_eq) | Ground-state total-Casimir value is the predicted value (overlap pin): Tasaki’s overlap step (§2.5, eq. 2.5.12). Given a Marshall-positive total-Casimir eigenvector at the predicted value tasaki23PredictedCasimirValue A N in sector M (the toy-Hamiltonian ground state), the per-sector Perron–Frobenius ground state Φ = magSectorEmbedding (marshallSignS · v) is itself a total-Casimir eigenvector at exactly the predicted value: Φ is a Casimir eigenvector at some real γ (tasaki23_pf_groundState_casimir_eigenvector + the Hermitian-eigenvalue realness lemma isHermitian_eigenvalue_star_eq), the Marshall-positive overlap with the witness is non-zero, so tasaki23_marshallPositive_casimir_eigenvalue_eq forces γ = predicted. This pins the ground-state total spin, leaving only the existence of the predicted-Casimir witness (the toy GS) as input. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (files Quantum/SpinS/Theorem23StructuralPFCasimirPredicted.lean (witness), Quantum/SpinS/Theorem23PFCasimirPredicted.lean (isHermitian_eigenvalue_star_eq)) |
| tasaki23_pf_groundState_ladder_link_of_casimir_ne_kernel | Adjacent-sector ladder link for the Perron ground state from Casimir non-vanishing: the per-sector Marshall-positive ground state Φ = magSectorEmbedding (marshallSignS · v) (v > 0, Ĥ Φ = μ Φ) satisfies the ladder link as soon as its (automatically existing, by tasaki23_pf_groundState_casimir_eigenvector) total-Casimir eigenvalue is away from the lowering-kernel value: Ŝ⁻_tot · Φ is a non-zero Heisenberg eigenvector at the same μ in the next sector. Replaces the predicted-GS-membership hypothesis of tasaki23_pf_ladder_link_succ_of_mem_predictedGS by the minimal Casimir-non-vanishing condition, so the sound chain applies directly to the actual ground state. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23PFCasimirEigenvector.lean) |
| tasaki23_pf_groundState_casimir_eigenvector | The per-sector Perron–Frobenius ground state is a total-Casimir eigenvector: the Marshall-positive Heisenberg sector ground state Φ = magSectorEmbedding (marshallSignS · v) (v > 0, Ĥ Φ = μ Φ) satisfies (Ŝtot)² Φ = γ Φ for some γ : ℂ. Since [Ĥ,(Ŝtot)²]=0 (heisenbergHamiltonianS_commute_totalSpinSSquared), (Ŝtot)² Φ is a Heisenberg eigenvector at the same μ in the same sector; its real and imaginary parts are real Heisenberg sector eigenvectors at μ, each a scalar multiple of Φ’s Marshall-positive form by the one-dimensionality tasaki23_heis_sector_eigenvec_proportional_of_marshallPositive, so recombining gives (Ŝtot)² Φ = γ Φ. This pins the total spin of the ground state (total-spin determination, Tasaki §2.5 p.42). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23StructuralPFJointCasimir.lean) |
| tasaki23_shiftedDressed_sector_eigenvec_proportional / tasaki23_heis_sector_eigenvec_proportional_of_marshallPositive | One-dimensionality of the Heisenberg sector ground eigenspace: the shifted dressed Heisenberg sector matrix is irreducible, so (geometric simplicity, PerronFrobenius.eigenvec_proportional_of_pos_eigenvec) any real eigenvector at the Perron eigenvalue is a scalar multiple of the positive Perron eigenvector. Marshall-conjugating, if φ is a Marshall-positive Heisenberg sector eigenvector at μ then every real Heisenberg sector eigenvector at μ is s • φ. This makes the per-sector Marshall-positive ground state the unique (up to scale) eigenvector at its energy — the step that will show it is a (Ŝtot)² eigenvector (total-spin determination). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23StructuralCasimirEigenvec.lean) |
| tasaki23_marshallPositive_casimir_eigenvalue_eq (with tasaki23_marshallPositive_sector_dotProduct_pos, tasaki23_magSectorEmbedding_dotProduct, tasaki23_marshallPositive_overlap_ne_zero) | Marshall-positive total-Casimir transfer (Tasaki’s overlap argument): two Marshall-positive sector vectors magSectorEmbedding (marshallSignS · v), magSectorEmbedding (marshallSignS · w) (v, w > 0) in the same non-empty sector that are total-Casimir (Ŝtot)² eigenvectors at real α, β must satisfy α = β. The Marshall signs cancel termwise, so the conjugate overlap collapses to the positive real sum ∑ v·w > 0 (hence non-zero); the orthogonality of (Ŝtot)² eigenvectors at distinct eigenvalues (Matrix.IsHermitian.dotProduct_eq_zero_of_eigenvalues_ne + totalSpinSSquared_isHermitian) then forces α = β. This is the bridge that will transfer the predicted total spin from the toy-Hamiltonian ground state to the antiferromagnetic Perron–Frobenius ground state (total-spin determination). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23PFTotalSpin.lean) |
| tasaki23_pf_sector_energy_eq | Sound PF adjacent-sector ground-energy constancy: combines the lowering and raising bounds into μ_M = μ_{M+1} for two adjacent admissible sectors interior to the range. Each sector’s Marshall-positive ground state marshallSignS · v (v > 0) is supplied both as a full-space Heisenberg eigenvector (magSectorEmbedding form) and a real-form sector-matrix eigenvector, with predicted-GS membership; le_antisymm of the two bounds gives equality. The inductive constancy step of the common-energy chain (sound route), still modulo the predicted-GS membership of the per-sector ground states. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23PFConstancy.lean) |
| tasaki23_pf_sector_energy_pred_le | Sound PF adjacent-sector ground-energy bound (raising): raising companion of tasaki23_pf_sector_energy_succ_le. If a predicted-GS Heisenberg eigenvector sits at μ in admissible sector M+1 strictly above the left endpoint and sector M carries a Marshall-positive real eigenvector at μ', then μ' ≤ μ. With the lowering bound this gives μ_M = μ_{M+1} (sector ground-energy constancy / common-energy chain). Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23PFConstancy.lean) |
| tasaki23_pf_sector_energy_succ_le | Sound PF adjacent-sector ground-energy bound (lowering): under |¬A| ≤ |A|, if a predicted-GS Heisenberg eigenvector magSectorEmbedding Φ sits at energy μ in an admissible sector M below the right endpoint, and sector M+1 carries a Marshall-positive real eigenvector w at energy μ', then μ' ≤ μ. Proof: the ladder link (tasaki23_pf_ladder_link_succ_of_mem_predictedGS) gives Ŝ⁻_tot · magSectorEmbedding Φ a non-zero same-μ eigenvector in sector M+1; its sector restriction is a non-zero complex sector eigenvector at μ, so a real/imaginary part is a non-zero real-form sector eigenvector at μ, which the Marshall-positive spectral lower bound (heisenbergHamiltonianSReMatrixOnMagSector_eigenvalue_ge_of_marshallPositive) bounds below by μ'. Half of the sector ground-energy constancy (common-energy chain), using no Marshall positivity of the lowered vector. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23PFConstancy.lean) |
| tasaki23_pf_ladder_link_succ_of_mem_predictedGS | Ladder link with Casimir hypotheses discharged via predicted-GS membership: specialises tasaki23_pf_ladder_link_succ to a sector vector lying in bipartiteToyGroundStateSubspacePredicted A N. Under |¬A| ≤ |A|, predicted-GS membership pins the total-Casimir eigenvalue to tasaki23PredictedCasimirValue A N (tasaki23_totalSpinSSquared_mulVec_of_mem_bipartiteToyGroundStateSubspacePredicted), which differs from the lowering-kernel value of any admissible sector M below the right endpoint (tasaki23_predictedCasimirValue_ne_lowering_kernel_value_of_mem_of_lt_right). Hence a predicted-GS Heisenberg eigenvector at μ in such a sector has Ŝ⁻_tot · Ψ a non-zero Heisenberg eigenvector at the same μ in sector M+1, with no remaining abstract Casimir input. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23PFLadderLink.lean) |
| magConfigS V N M | sector subtype of magnetization-M configurations (Quantum/SpinS/MagConfig.lean) |
| RaiseLowerStepSMagSector G σ τ / RaiseLowerReachableSMagSector G | bipartite raise/lower step lifted to magConfigS and its reflexive transitive closure (Quantum/SpinS/MagConfig.lean) |
| raiseLowerReachableSMagSector_bipartiteCompleteGraph | any two configurations in the same sector are reachable via raise/lower steps under the bipartite-intermediate hypothesis (Tasaki §2.5 Property (iii) generic-S form) |
| shiftedDressedSReMatrixOnMagSector A J N c M | shifted dressed Heisenberg matrix c·1 - dressed_re restricted to the sector via Matrix.submatrix Subtype.val Subtype.val, the input to PF irreducibility |
| dressedHeisenbergSReMatrixOnMagSector A J N M | dressed Heisenberg real-form matrix restricted to the sector |
| heisenbergHamiltonianSReMatrixOnMagSector J N M | un-dressed Heisenberg real-form matrix restricted to the sector |
| heisenbergHamiltonianSMatrixOnMagSector J N M | un-dressed Heisenberg COMPLEX matrix restricted to the sector |
| isIrreducible_shiftedDressedSReMatrixOnMagSector | Matrix.IsIrreducible for the shifted sector matrix (Tasaki §2.5 γ-3 final, MLM PF input) |
| exists_positive_eigenvector_shiftedDressedSReMatrixOnMagSector | PF eigenvector existence for the shifted sector matrix (r > 0, v > 0 componentwise) |
| pos_eigenvec_unique_shiftedDressedSReMatrixOnMagSector | PF eigenvector uniqueness on the shifted sector matrix (Tasaki §2.5 nondegeneracy) |
| exists_positive_eigenvector_dressedHeisenbergSReMatrixOnMagSector | PF on the dressed sector matrix at eigenvalue c - r (Tasaki §2.5 dressed-form ground state) |
| pos_eigenvec_unique_dressedHeisenbergSReMatrixOnMagSector | dressed sector eigenvector uniqueness at fixed eigenvalue (PR #856) |
| pos_eigenvec_eigenvalue_unique_dressedHeisenbergSReMatrixOnMagSector | dressed sector positive eigenvectors share the same eigenvalue (Rayleigh identity for symmetric matrices, PR #856) |
| dressedHeisenbergSReMatrix_eq_marshallSign_mul_heisenberg / heisenbergHamiltonianSReMatrix_eq_marshallSign_mul_dressed | matrix relations dressed = sign·sign·heis and inverse via sign² = 1 (PR #853) |
| marshallSignS_mul_of_agree_off_site / marshallSignS_mul_of_agree_off_site_A_true_lower / marshallSignS_mul_of_agree_off_site_A_false_lower / marshallSignS_re_mul_re_of_agree_off_site_A_true_lower / marshallSignS_re_mul_re_of_agree_off_site_A_false_lower | Single-site Marshall sign bookkeeping for Tasaki §2.5 Theorem 2.3 lowered-vector predecessors: if a target configuration σ' and predecessor σ agree away from one site x, the product of their Marshall signs factors through the single site. For a lowering predecessor (σ x).val + 1 = (σ' x).val, the sign product is -1 when x ∈ A and 1 when x ∉ A, with matching real-part identities. This is the local sign input for the site-sum positivity proof of the lowered vector in the adjacent-sector ladder step. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/MarshallSignCore.lean) |
| marshallDressedBasisS A σ | Spin-S Marshall-dressed basis state := marshallSignS A σ • basisVecS σ, generalising the spin-1/2 marshallDressedBasis (Tasaki §2.5 eq. (2.5.8), p. 41) to arbitrary spin S via the marshallSignS/basisVecS spin-S primitives. Component rules (_apply, _self, _of_ne), the all-zero specialisation (_const_zero), orthonormality (_inner_product), magnetization-subspace membership (_mem_magSubspaceS), the sign-inverse identity marshallSignS A σ • marshallDressedBasisS A σ = basisVecS σ, and non-vanishing (_ne_zero) — the spin-S counterpart of the marshallDressedBasis row above; exercised by Tests/SpinSMarshallSign.lean (not yet consumed by another production module) (file Quantum/SpinS/MarshallSign.lean) |
| heisenbergHamiltonianSReMatrixOnMagSector_mulVec_of_dressed_eigenvec | Marshall sign conjugation of dressed sector eigenvector to un-dressed Heisenberg sector eigenvector (PR #853) |
| dressedHeisenbergSReMatrixOnMagSector_mulVec_of_heis_eigenvec | inverse Marshall conjugation (PR #854) |
| exists_marshallSign_eigenvector_heisenbergHamiltonianSReMatrixOnMagSector | un-dressed Heisenberg sector ground-state existence with Marshall sign structure (PR #853) |
| marshallPositive_eigenvec_unique_heisenbergHamiltonianSReMatrixOnMagSector | un-dressed Heisenberg sector Marshall-positive eigenvector uniqueness at fixed eigenvalue (PR #854) |
| marshallPositive_eigenvec_eigenvalue_unique_heisenbergHamiltonianSReMatrixOnMagSector | un-dressed Heisenberg sector Marshall-positive eigenvalue uniqueness (PR #856) |
| marshallLiebMattis_spinS_heisenbergSector_groundState | bundled Tasaki §2.5 Theorem 2.2 (existence + same-eigenvalue uniqueness, PR #855; relocated to Quantum/SpinS/MarshallLiebMattisSectorBundled.lean in #4569) |
| marshallLiebMattis_spinS_heisenbergSector_groundState_full | strongest bundled Tasaki §2.5 Theorem 2.2: existence + forced eigenvalue uniqueness + eigenvector uniqueness (PR #859) |
| heisenbergHamiltonianSMatrixOnMagSector_isHermitian | complex sector matrix is Hermitian for real coupling (PR #858) |
| heisenbergHamiltonianSMatrixOnMagSector_apply_eq_ofReal | for real coupling, complex sector entries equal real-form entries embedded in ℂ (PR #857) |
| heisenbergHamiltonianSMatrixOnMagSector_mulVec_ofReal | real → complex eigenvector lift (PR #858) |
| heisenbergHamiltonianSReMatrixOnMagSector_mulVec_re_of_complex_eigenvec | complex → real real-part extraction (PR #861) |
| exists_marshallSign_complexEigenvector_heisenbergHamiltonianSMatrixOnMagSector | complex-form Tasaki §2.5 Theorem 2.2 ground-state existence on the un-dressed quantum Heisenberg sector matrix (PR #860) |
| marshallPositive_complexEigenvec_re_unique_heisenbergHamiltonianSMatrixOnMagSector | complex-form Marshall-positive uniqueness via real-part extraction (PR #862) |
| marshallLiebMattis_spinS_heisenbergSector_complexGroundState_full | strongest bundled Tasaki §2.5 Theorem 2.2 on the complex sector matrix (PR #863; relocated to Quantum/SpinS/MarshallLiebMattisSectorBundled.lean in #4569) |
| tasaki_2_5_theorem_2_3 / tasaki23PredictedTotalSpin / tasaki23PredictedDegeneracy / tasaki23GroundStateSectors | Tasaki §2.5 Theorem 2.3 (Lieb–Mattis, general spin-S, \|A\| ≠ \|¬A\|), final statement as a Prop definition. The hypothesis bundle and conclusion match the per-sector bundled Theorem 2.2 marshallLiebMattis_spinS_heisenbergHamiltonianS_groundState_full (#869) exactly — real symmetric coupling ((J x y).im = 0, star (J x y) = J x y, J x y = J y x, 0 ≤ (J x y).re), bipartite support, positivity on bipartiteCompleteGraphOf A, non-empty sublattices, a spectral shift c strictly above the dressed diagonal, the #869 intermediate-existence hypothesis, plus sector non-emptiness — and asserts existence of a common GS energy μ realised on every admissible sector M ∈ tasaki23GroundStateSectors A N by a Marshall-positive eigenvector (Tasaki (2.5.4) with σ = M), with within-sector uniqueness up to positive scalar, plus global minimality of μ. Together with tasaki23PredictedDegeneracy A N = \|\|A\| − \|¬A\|\|·N + 1 = 2 S_tot + 1 (cardinality of tasaki23GroundStateSectors A N), this packages the predicted total spin S_tot = \|\|A\| − \|¬A\|\|·N/2 and the predicted 2 S_tot + 1 degeneracy. Proof: iterate #869 across tasaki23GroundStateSectors A N. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (PR #3337, files Quantum/SpinS/Theorem23StructuralBipartiteToy.lean, Quantum/SpinS/Theorem23Sectors.lean) |
| tasaki23GroundStateSectors_mem_iff / _left_mem / _right_mem / _succ_mem_of_mem_of_lt_right / _pred_mem_of_left_lt_of_mem / _card | Tasaki §2.5 Theorem 2.3 admissible-sector interval combinatorics: membership in tasaki23GroundStateSectors A N is exactly the closed integer interval [min(\|A\|,\|¬A\|)·N, max(\|A\|,\|¬A\|)·N]; both endpoints belong to the interval; every non-right-endpoint sector has its successor in the interval; every non-left-endpoint sector has its predecessor in the interval; and the interval cardinality is the predicted degeneracy tasaki23PredictedDegeneracy A N = \|\|A\| − \|¬A\|\|·N + 1 = 2 S_tot + 1. These are the finite-range bookkeeping lemmas used to iterate the lowering/raising adjacent-sector energy comparisons across the Theorem 2.3 multiplet. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23Sectors.lean) |
| tasaki23PredictedCasimirValue / tasaki23_card_filter_A_add_card_notA / tasaki23PredictedTotalSpin_eq_sector_half_width / tasaki23_lowering_kernel_value_lt_predictedCasimirValue_of_mem_of_lt_right / tasaki23_raising_kernel_value_lt_predictedCasimirValue_of_mem_of_left_lt / tasaki23_predictedCasimirValue_ne_lowering_kernel_value_of_mem_of_lt_right / tasaki23_predictedCasimirValue_ne_raising_kernel_value_of_mem_of_left_lt | Tasaki §2.5 Theorem 2.3 predicted-Casimir endpoint mismatch: the predicted total-Casimir value is S_tot(S_tot+1), where S_tot is half the width of the admissible sector interval; the partition lemma records \|A\| + \|¬A\| = \|V\| for the two sublattices. If M is admissible and strictly before the right endpoint, the real lowering-kernel endpoint value for m = \|V\|N/2 - M is strictly below the predicted value, hence not equal after coercion to ℂ; dually, if M+1 is admissible and strictly above the left endpoint, the raising-kernel endpoint value is strictly below the predicted value and therefore not equal. These lemmas discharge the concrete hγ_ne hypotheses in the Casimir non-vanishing successor/predecessor wrappers once the source sector vector is known to have the predicted total-Casimir eigenvalue. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (files Quantum/SpinS/Theorem23Sectors.lean, Quantum/SpinS/Theorem23PredictedEndpoint.lean) |
| tasaki23PredictedCasimirValue_eq_canonical_of_card_notA_le_cardA / tasaki23_totalSpinSSquared_mulVec_of_mem_bipartiteToyGroundStateSubspacePredicted | Tasaki §2.5 Theorem 2.3 predicted-GS total-Casimir bridge: in the canonical orientation \|¬A\| ≤ \|A\|, the absolute value in the predicted total spin drops to \|A\| - \|¬A\|, so tasaki23PredictedCasimirValue A N equals the canonical total-Casimir target in bipartiteToyGroundStateSubspacePredicted A N. Consequently, any vector in the predicted toy ground-state subspace is a totalSpinSSquared eigenvector with eigenvalue tasaki23PredictedCasimirValue A N. This is the exact source-sector Casimir hypothesis needed by the adjacent-sector Theorem 2.3 chain once membership in the predicted toy ground-state subspace is available. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23Predicted.lean) |
| totalSpinSOp3_mulVec_apply_eq_magEigenvalueS_mul / magSectorEmbedding_mem_magSubspaceS / magSubspaceS_apply_eq_zero_of_magSumS_ne / magSectorEmbedding_magSectorRestriction_of_mem_magSubspaceS / totalSpinSOpMinus_mulVec_magSectorEmbedding_supported_succ / totalSpinSOpPlus_mulVec_magSectorEmbedding_supported_pred | Tasaki §2.5 Theorem 2.3 sector-support bridge and adjacent-sector ladder shifts: Ŝ_tot^(3) acts diagonally on arbitrary full spin-S vectors, zero-extended magSumS = M sector vectors lie in the Ŝ_tot^(3) eigenspace \|V\|·N/2 - M, and an Ŝ_tot^(3) eigenspace vector vanishes outside the matching magSumS sector. Such a full eigenspace vector is therefore exactly the zero-extension of its sector restriction, letting later component arguments reuse the sector-embedding APIs for vectors obtained from successor magSubspaceS support. Consequently Ŝ^-_tot maps an embedded sector vector supported on M to a full vector supported on M + 1, while Ŝ^+_tot maps an embedded sector vector supported on M + 1 back to sector M. These are the support halves of the adjacent-sector comparisons used with ladder eigenvalue preservation. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (files Quantum/SpinS/MagSectorEmbedding.lean, Quantum/SpinS/Theorem23Local.lean) |
| heisenbergHamiltonianS_mulVec_totalSpinSOpMinus_of_eigenvec / heisenbergHamiltonianS_mulVec_totalSpinSOpPlus_of_eigenvec | Tasaki §2.5 Theorem 2.3 ladder eigenvalue preservation: if Ψ is a Heisenberg eigenvector at real eigenvalue μ, then Ŝ^-_tot Ψ and Ŝ^+_tot Ψ are Heisenberg eigenvectors at the same eigenvalue. These are the one-step SU(2) ladder facts used to compare adjacent magnetization-sector ground-state eigenvalues in the Theorem 2.3 multiplet. Directly from [H, Ŝ_tot^±] = 0 (heisenbergHamiltonianS_commute_totalSpinSOpMinus/Plus) and Matrix.mulVec_mulVec. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23Local.lean) |
| tasaki23_totalSpinSSquared_mulVec_of_totalSpinSOpMinus_eq_zero_of_mem_magSubspaceS / tasaki23_totalSpinSSquared_mulVec_of_totalSpinSOpPlus_eq_zero_of_mem_magSubspaceS | Tasaki §2.5 Theorem 2.3 ladder-kernel Casimir consequences: if a vector in the Ŝ_tot^(3) eigenspace of eigenvalue m is killed by Ŝ^-_tot, then it is a total-Casimir eigenvector with eigenvalue m * (m - 1); if it is killed by Ŝ^+_tot, then the forced total-Casimir eigenvalue is m * (m + 1). These are the SU(2) obstruction statements for a vanished adjacent-sector ladder move, proved from the total-spin Casimir rearrangements Ŝ^+Ŝ^- = Ŝ² - (Ŝ^z)² + Ŝ^z and Ŝ^-Ŝ^+ = Ŝ² - (Ŝ^z)² - Ŝ^z. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23Casimir.lean) |
| tasaki23_totalSpinSOpMinus_mulVec_ne_zero_of_casimir_ne_kernel_value / tasaki23_totalSpinSOpPlus_mulVec_ne_zero_of_casimir_ne_kernel_value | Tasaki §2.5 Theorem 2.3 Casimir-based ladder non-vanishing: if a nonzero vector in the Ŝ_tot^(3) eigenspace of eigenvalue m has total-Casimir eigenvalue γ, then γ ≠ m * (m - 1) forces Ŝ^-_tot Ψ ≠ 0, and γ ≠ m * (m + 1) forces Ŝ^+_tot Ψ ≠ 0. These are the contrapositive forms of the ladder-kernel Casimir consequences and are the bridge from the SU(2) obstruction to the sector interval argument: away from the representation endpoint value, the adjacent-sector ladder move cannot vanish. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23Casimir.lean) |
| tasaki23_totalSpinSOpMinus_mulVec_magSectorEmbedding_ne_zero_of_casimir_ne_kernel_value / tasaki23_totalSpinSOpPlus_mulVec_magSectorEmbedding_ne_zero_of_casimir_ne_kernel_value | Tasaki §2.5 Theorem 2.3 sector-embedded Casimir ladder non-vanishing: the Casimir-based non-vanishing criteria are specialized to zero-extended magSumS = M sector vectors. If magSectorEmbedding Φ is a nonzero total-Casimir eigenvector at value γ, then γ different from the lowering endpoint value for \|V\|·N/2 - M forces Ŝ^-_tot (magSectorEmbedding Φ) ≠ 0, and γ different from the raising endpoint value forces Ŝ^+_tot (magSectorEmbedding Φ) ≠ 0. This packages the abstract magSubspaceS obstruction with magSectorEmbedding_mem_magSubspaceS, making it directly usable in the adjacent-sector chain. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23Casimir.lean) |
| tasaki23_marshallPositive_magSectorEmbedding_ne_zero / t23_totSpinSOpMinus_mulVec_marshPos_magSecEmb_ne_zero_of_cas_ne_kernelVal / t23_totSpinSOpPlus_mulVec_marshPos_magSecEmb_ne_zero_of_cas_ne_kernelVal | Tasaki §2.5 Theorem 2.3 Marshall-positive sector Casimir ladder non-vanishing: a sector vector with strictly positive Marshall coefficients has nonzero zero-extension, because its value at any sector configuration is a nonzero real multiple of the Marshall sign. Consequently the sector-embedded Casimir non-vanishing criteria apply directly to the Theorem 2.2 Marshall-positive sector ground-state vector: a non-endpoint total-Casimir eigenvalue forces the corresponding lowering or raising image to be nonzero. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23Casimir.lean) |
| tasaki23_lowered_ne_zero_of_marshall_pos / totalSpinSOpMinus_mulVec_magSectorEmbedding_apply_eq_site_sum / tasaki23_lowered_marshall_pos_of_site_sum_pos / tasaki23_lowering_identifies_adjacent_sector_energy / tasaki23_lowering_identifies_adjacent_sector_energy_with_nonzero / tasaki23_lowering_identifies_adjacent_sector_energy_of_site_sum_pos | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. |
| tasaki23_raised_ne_zero_of_marshall_pos / tasaki23_raised_marshall_pos_of_site_sum_pos / tasaki23_raising_identifies_adjacent_sector_energy / tasaki23_raising_identifies_adjacent_sector_energy_with_nonzero / tasaki23_raising_identifies_adjacent_sector_energy_of_site_sum_pos | Tasaki §2.5 Theorem 2.3 adjacent-sector energy identification, conditional raising step with non-vanishing and site-sum positivity form: if an embedded magSumS = M + 1 source-sector eigenvector has eigenvalue μ, and its raised vector Ŝ^+_tot Ψ_{M+1} satisfies the Marshall-positive hypothesis in the adjacent sector M, then strict positivity already implies Ŝ^+_tot Ψ_{M+1} ≠ 0, and the full-Hilbert-space Theorem 2.2 uniqueness clause in sector M identifies the target sector eigenvalue with μ. The raised component can also be invoked from the local site-sum strict positivity hypothesis for ∑ x, Ŝ^+_x Ψ_{M+1}. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23Local.lean for the surviving subject tasaki23_raised_ne_zero_of_marshall_pos; tasaki23_raised_marshall_pos_of_site_sum_pos lived in Quantum/SpinS/Theorem23LocalDifferenceMarshall.lean, tasaki23_raising_identifies_adjacent_sector_energy and tasaki23_raising_identifies_adjacent_sector_energy_with_nonzero lived in Quantum/SpinS/Theorem23LocalDifferenceEnergy.lean, and tasaki23_raising_identifies_adjacent_sector_energy_of_site_sum_pos lived in Quantum/SpinS/Theorem23LocalDifferenceEnergyCasimir.lean, all three deleted in PR #3919 (bulk orphan-module deletion)) |
| totalSpinSOpPlus_mulVec_magSectorEmbedding_apply_eq_site_sum / onSiteS_spinSOpPlus_mulVec_magSectorEmbedding_apply_eq_zero_of_target_top / onSiteS_spinSOpPlus_mulVec_magSectorEmbedding_apply_single_site_succ / onSiteS_spinSOpPlus_mulVec_magSectorEmbedding_apply_single_site_succ_re / tasaki23_signed_single_site_raising_component_pos_of_A_false / tasaki23_signed_single_site_raising_component_neg_of_A_true | Single-site raising component formula and local signed contribution split for Tasaki §2.5 Theorem 2.3: the x-summand of Ŝ^+_tot at a target sector configuration τ : magConfigS V N M is zero when (τ x).val = N; when (τ x).val < N, it is exactly the spinSOpPlus matrix coefficient times the source-sector coefficient at the unique successor obtained by replacing τ x with (τ x).val + 1, and its real part is the positive raising coefficient times the successor coefficient’s real part. Under source-sector Marshall positivity, the signed real contribution is strictly positive for A x = false and strictly negative for A x = true, matching the same one-site Marshall sign product as the lowering predecessor case. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23LocalRaisedSiteSum.lean for the surviving subject totalSpinSOpPlus_mulVec_magSectorEmbedding_apply_eq_site_sum; onSiteS_spinSOpPlus_mulVec_magSectorEmbedding_apply_eq_zero_of_target_top, onSiteS_spinSOpPlus_mulVec_magSectorEmbedding_apply_single_site_succ and onSiteS_spinSOpPlus_mulVec_magSectorEmbedding_apply_single_site_succ_re lived in Quantum/SpinS/Theorem23LocalDifferenceRaising.lean, and tasaki23_signed_single_site_raising_component_pos_of_A_false and tasaki23_signed_single_site_raising_component_neg_of_A_true lived in Quantum/SpinS/Theorem23LocalDifferenceRaisingPositivity.lean, both deleted in PR #3919 (bulk orphan-module deletion)) |
| sublatticeSpinSOpMinus_mulVec_magSectorEmbedding_apply_eq_onA_site_sum / sublatticeSpinSOpMinus_complement_mulVec_magSectorEmbedding_apply_eq_offA_site_sum / tasaki23_signed_lowering_offA_sublattice_component_eq_coefficient_sum / tasaki23_signed_lowering_onA_sublattice_component_eq_neg_coefficient_sum | Sublattice lowered coefficient components for Tasaki §2.5 Theorem 2.3: the filtered lowering sums are identified with the actual sublattice ladder operators Ŝ_A^- and Ŝ_¬A^-. After multiplying by the Marshall sign, the Ŝ_¬A^- component is exactly the off-A predecessor-coefficient sum, while the Ŝ_A^- component is the negative of the on-A predecessor-coefficient sum. This connects the remaining coefficient dominance input to the operator-level sublattice ladder components needed for the predicted-GS/Casimir argument. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23Local.lean for the two surviving sublatticeSpinSOpMinus_* subjects; tasaki23_signed_lowering_offA_sublattice_component_eq_coefficient_sum and tasaki23_signed_lowering_onA_sublattice_component_eq_neg_coefficient_sum lived in Quantum/SpinS/Theorem23LocalDifference.lean, deleted in PR #3919 (bulk orphan-module deletion)) |
| tasaki23_sublatticeSpinSquaredS_mulVec_of_mem_bipartiteToyGroundStateSubspacePredicted / t23_sublatSpinS2_complement_mulVec_of_mem_bipToyGSPred / tasaki23_lowered_sublatticeSpinSquaredS_of_mem_bipartiteToyGroundStateSubspacePredicted / tasaki23_lowered_sublatticeSpinSquaredS_complement_of_mem_bipartiteToyGroundStateSubspacePredicted | Predicted-GS sublattice Casimir bridges for Tasaki §2.5 Theorem 2.3: predicted toy ground-state membership is unpacked into the two maximum sublattice-Casimir eigenvector identities (Ŝ_A)^2 = s_A(s_A+1) and (Ŝ_¬A)^2 = s_B(s_B+1). The same identities are also transported to the total-lowering image by predicted-GS lowering closure. This gives the Casimir-side hypotheses needed to prove the sublattice lowering component comparison from the predicted-GS structure. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23Predicted.lean for the two surviving unpacking subjects; tasaki23_lowered_sublatticeSpinSquaredS_of_mem_bipartiteToyGroundStateSubspacePredicted and tasaki23_lowered_sublatticeSpinSquaredS_complement_of_mem_bipartiteToyGroundStateSubspacePredicted lived in Quantum/SpinS/Theorem23PredictedLadder.lean, deleted in PR #3919 (bulk orphan-module deletion)) |
| sublatticeSpinSDot_eq_op3_add_ladder / tasaki23_heisenbergToyHamiltonianS_mulVec_of_mem_bipartiteToyGroundStateSubspacePredicted / tasaki23_two_sublatticeSpinSDot_mulVec_of_mem_bipartiteToyGroundStateSubspacePredicted / tasaki23_two_cross_ladder_mulVec_of_mem_bipartiteToyGroundStateSubspacePredicted / tasaki23_cross_ladder_sum_mulVec_eq_energy_sub_two_op3_of_predictedGS / tasaki23_cross_ladder_sequential_mulVec_eq_energy_sub_two_op3_of_predictedGS / tasaki23_cross_ladder_raised_lowered_components_eq_energy_sub_two_op3_of_predictedGS | Predicted-GS toy cross-ladder bridges for Tasaki §2.5 Theorem 2.3: predicted toy ground-state membership is also unpacked into the pointwise toy-Hamiltonian eigenvector identity at bipartiteToyMinEnergyPredicted A N. Using Ĥ_toy_S = 2 • Ŝ_A · Ŝ_¬A, this yields the corresponding eigenvector identity for the cross-sublattice spin-dot operator, and sublatticeSpinSDot_eq_op3_add_ladder rewrites that dot product as Ŝ_A^3 Ŝ_¬A^3 + (1/2)(Ŝ_A^+ Ŝ_¬A^- + Ŝ_A^- Ŝ_¬A^+). The isolated ladder-sum corollary moves Ŝ_A^+ Ŝ_¬A^- + Ŝ_A^- Ŝ_¬A^+ to the left-hand side as the predicted toy-energy term minus twice the Ŝ_A^3 Ŝ_¬A^3 contribution, the sequential form rewrites that left side as Ŝ_A^+(Ŝ_¬A^- Ψ) + Ŝ_A^-(Ŝ_¬A^+ Ψ), and the raised-lowered component form commutes the second term to Ŝ_¬A^+(Ŝ_A^- Ψ). This is the operator bridge needed for comparing the A and ¬A lowering components. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (files Quantum/SpinS/SublatticeSpinDot.lean, Quantum/SpinS/Theorem23Predicted.lean) |
| sublatticeSpinSOpPlus_mulVec_magSectorEmbedding_apply_eq_onA_site_sum / sublatticeSpinSOpPlus_complement_mulVec_magSectorEmbedding_apply_eq_offA_site_sum / tasaki23_cross_ladder_reembedded_source_site_sum_eq_energy_sub_two_op3_of_predictedGS | Re-embedded cross-ladder source-sector site sums for Tasaki §2.5 Theorem 2.3: the sublattice raising operators Ŝ_A^+ and Ŝ_¬A^+ are expanded over the filtered site sums on A and outside A when applied to an embedded successor-sector vector. Combining these expansions with magSectorEmbedding_magSectorRestriction_of_mem_magSubspaceS rewrites the predicted-GS raised-lowered cross-ladder identity at a source-sector configuration in terms of the sector restrictions of the two lowered components Ŝ_A^- Ψ and Ŝ_¬A^- Ψ. This is the component-level bridge needed before proving the local Marshall-signed coefficient comparison from the cross-ladder equation. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (files Quantum/SpinS/MagSectorEmbedding.lean, Quantum/SpinS/Theorem23LocalRaisedSiteSum.lean, Quantum/SpinS/Theorem23Predicted.lean) |
| tasaki23GroundStateSectors_le_card_mul / tasaki_2_5_theorem_2_3_of_physical_range_nonempty_threaded_predictedGS_of_unpacked_reembedded_real_source_weight_predecessor_difference_pos_of_outside_sector_ground_energy_lower_bound | Physical-range non-empty boundary for Tasaki §2.5 Theorem 2.3: every admissible sector in tasaki23GroundStateSectors A N lies in the full magnetization range M ≤ Fintype.card V * N, because the right endpoint is bounded by (|A| + |¬A|) * N = |V| * N. The final boundary uses this range lemma to replace the interval-specific magConfigS non-emptiness callback by a canonical physical-range non-emptiness callback, while keeping the threaded predicted-GS input, local predecessor-difference comparison, and outside-sector ground-representative lower bounds. Internally it now discharges the non-emptiness input and invokes the explicit source common-energy final boundary directly. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42; Seneta, Non-negative Matrices and Markov Chains, 3rd ed., Springer 2006, §1.2, pp. 27–28 (file Quantum/SpinS/Theorem23Sectors.lean for the surviving subject tasaki23GroundStateSectors_le_card_mul; the wrapper tasaki_2_5_theorem_2_3_of_physical_range_nonempty_threaded_predictedGS_of_unpacked_reembedded_real_source_weight_predecessor_difference_pos_of_outside_sector_ground_energy_lower_bound lived in Quantum/SpinS/Theorem23Final.lean, deleted in PR #3645 (unsound saturated-ladder Theorem 2.3 route)) |
| heisenbergHamiltonianS_mulVec_totalSpinSOpMinus_pow_of_eigenvec / heisenbergHamiltonianS_mulVec_totalSpinSOpPlus_pow_of_eigenvec / totalSpinSOpMinus_pow_mulVec_mem_magSubspaceS_of_mem / totalSpinSOpPlus_pow_mulVec_mem_magSubspaceS_of_mem / tasaki23OutsideGroundLeftIteratedLadderFullReachCallback / tasaki23OutsideGroundRightIteratedLadderFullReachCallback / tasaki23OutsideGroundAdmissibleFullReachCallback_of_iterated_ladder_callbacks / tasaki23OutsideGroundEnergyLowerFamilyCallback_of_iterated_ladder_full_reach / tasaki_2_5_theorem_2_3_of_threaded_predictedGS_of_unpacked_reembedded_real_source_weight_predecessor_difference_pos_of_iterated_ladder_full_reach_discharge_nonempty | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. |
| tasaki23GroundStateSectors_not_mem_iff_lt_left_or_right_lt / tasaki23OutsideGroundLeftAdmissibleReachCallback / tasaki23OutsideGroundRightAdmissibleReachCallback / tasaki23OutsideGroundAdmissibleReachCallback_of_side_callbacks | Outside-ground side split for Tasaki §2.5 Theorem 2.3: an outside magnetization sector is now decomposed arithmetically into the cases below the left endpoint and above the right endpoint of tasaki23GroundStateSectors A N. The full outside admissible-reach callback follows from separate left and right directional ladder-reach callbacks, exposing the lowering and raising sides of the remaining outside-sector reach task while preserving the public admissible-reach boundary used by the final wrappers. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42; Seneta, Non-negative Matrices and Markov Chains, 3rd ed., Springer 2006, §1.2, pp. 27–28 (file Quantum/SpinS/Theorem23Sectors.lean for the surviving subject tasaki23GroundStateSectors_not_mem_iff_lt_left_or_right_lt; tasaki23OutsideGroundLeftAdmissibleReachCallback, tasaki23OutsideGroundRightAdmissibleReachCallback and tasaki23OutsideGroundAdmissibleReachCallback_of_side_callbacks lived in Quantum/SpinS/Theorem23OutsideGround.lean, deleted in PR #3645 (unsound saturated-ladder Theorem 2.3 route)) |
| sublatticeSpinSquaredS_commute_sublatticeSpinSOpMinus / sublatticeSpinSquaredS_commute_sublatticeSpinSOpMinus_complement / tasaki23_sublatticeSpinSquaredS_sublatticeSpinSOpMinus_of_mem_bipartiteToyGroundStateSubspacePredicted / tasaki23_sublatticeSpinSquaredS_complement_sublatticeSpinSOpMinus_complement_of_mem_bipartiteToyGroundStateSubspacePredicted | Sublattice-ladder Casimir preservation for Tasaki §2.5 Theorem 2.3: the maximum sublattice-Casimir identities are transported from a predicted toy ground state to its individual A and ¬A lowering components. The support lemmas first record that (Ŝ_A)^2 commutes with Ŝ_A^- and with the complement lowering ladder; the Theorem 2.3 bridges then show Ŝ_A^- Φ and Ŝ_¬A^- Φ remain in the corresponding maximum sublattice-Casimir eigenspaces. This supplies the component-level Casimir input for the remaining comparison between the two sublattice lowering pieces. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/SublatticeSpinLadder.lean for the two surviving commutation lemmas; the bridges tasaki23_sublatticeSpinSquaredS_sublatticeSpinSOpMinus_of_mem_bipartiteToyGroundStateSubspacePredicted and tasaki23_sublatticeSpinSquaredS_complement_sublatticeSpinSOpMinus_complement_of_mem_bipartiteToyGroundStateSubspacePredicted lived in Quantum/SpinS/Theorem23PredictedLadder.lean, deleted in PR #3919 (bulk orphan-module deletion)) |
| totalSpinSSquared_mulVec_totalSpinSOpMinus_pow_of_eigenvec / totalSpinSSquared_mulVec_totalSpinSOpPlus_pow_of_eigenvec / totalSpinSOpMinus_pow_mulVec_ne_zero_of_casimir_ne_kernel_values / totalSpinSOpPlus_pow_mulVec_ne_zero_of_casimir_ne_kernel_values | Iterated total-spin ladder Casimir preservation and non-vanishing for Tasaki §2.5 Theorem 2.3: the preservation lemmas transport a total-Casimir eigenvalue through an iterated Ŝ_tot^- or Ŝ_tot^+ ladder. The non-vanishing lemmas then prove that the iterated ladder output remains nonzero whenever every intermediate magnetization avoids the corresponding one-step ladder-kernel Casimir value. Tasaki, Springer 2020, §2.5 Theorem 2.3, p. 42 (file Quantum/SpinS/Theorem23Local.lean) |
The complex-form marshallLiebMattis_spinS_heisenbergSector_complexGroundState_full
is the COMPLEX-Hilbert-space form of Tasaki §2.5 Theorem 2.2 in the
magnetization sector: the ground state of the un-dressed quantum
Heisenberg Hamiltonian restricted to the sector is unique (up to a
positive real scalar in its real part) and has the Marshall sign
structure Φ σ := ((sign A σ.1).re * v σ : ℂ) with v > 0.
tasaki_2_5_theorem_2_3 (PR #3337) is the final-statement form
of the |A| ≠ |¬A| case. The hypothesis bundle matches
marshallLiebMattis_spinS_heisenbergHamiltonianS_groundState_full
(#869) exactly. The conclusion bundles, per admissible sector
M ∈ tasaki23GroundStateSectors A N, the Marshall-positive
sector eigenvector existence and within-sector uniqueness from
#869, together with a global energy-minimality clause. The
predicted total spin and predicted degeneracy enter as the
cardinality identity |tasaki23GroundStateSectors A N| =
tasaki23PredictedDegeneracy A N = 2 S_tot + 1 with
S_tot = ||A| − |¬A||·N/2 = tasaki23PredictedTotalSpin A N. The
proof iterates #869 across tasaki23GroundStateSectors A N.
References: H. Tasaki, Physics and Mathematics of Quantum Many-Body Systems, Springer 2020, §2.5 Theorem 2.2 (pp. 39–43), Theorem 2.3 (p. 42); E. Seneta, Non-negative Matrices and Markov Chains (3rd ed.), Springer 2006, §1.2 (pp. 27–28) for the underlying Perron–Frobenius theorem.
← 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) →