Interim authority. This lossless catalogue chunk remains authoritative for formalization status and capstone identification until Issue #5228. The version 1 JSON catalogue is still a non-authoritative prototype.
Interim catalogue › Spin foundations and Tasaki Chapter 2
| Lean name | Statement | File |
|—|—|—|
| leafSpinSSquared_four | Pentamer (z=4) leaf-Casimir decomposition: leafSpinSSquared 4 N = N(N+2)·1 + 2·(spinSDot 1 2 + spinSDot 1 3 + spinSDot 1 4 + spinSDot 2 3 + spinSDot 2 4 + spinSDot 3 4) on Fin 5. Four diagonal spinSDot j j terms collapse via spinSDot_self; twelve off-diagonal pair up into six couplings via spinSDot_comm. Generalises γ-5 step 303 (z=3 quartet) to the pentamer (γ-5 step 312) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1359) |
| singleClusterHamiltonianS_eigenvalue_pentamer | Pentamer eigenvalue from Stot² + leaf-leaf sum: for z=4, joint eigenvector of Stot² (=α) and 6-pair sum (=γ) is an H-eigenvector at (α − 5N(N+2)/4 − 2γ)/2. Specialisation of γ-5 step 259 using γ-5 step 312 (γ-5 step 313) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1360) |
| singleClusterHamiltonianS_eigenvalue_pentamer_gs | Pentamer GS-sector at GS energy: for z=4, joint eigenvector at Stot²·v=(3N/2)(3N/2+1)·v (s_tot=3N/2) and 6-pair sum (3N²/2)·v (max leaf-spin s_R=2N) gives H · v = singleClusterGSEnergyS 4 N · v = -N(2N+1)/2 · v (γ-5 step 314) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1361) |
| singleClusterHamiltonianS_eigenvalue_pentamer_top | Pentamer top-spin sector at Max energy: for z=4, joint eigenvector at Stot²·v=(5N/2)(5N/2+1)·v (s_tot=5N/2=(z+1)N/2) and 6-pair sum (3N²/2)·v (max leaf-spin s_R=2N) gives H · v = singleClusterMaxEnergyS 4 N · v = N² · v (γ-5 step 315) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1362) |
| singleClusterHamiltonianS_eigenvalue_quartet_leaf_singlet | Quartet leaf-singlet sector eigenvalue = 0: for z=3, joint eigenvector at s_tot=N/2 and 3-pair sum (-3N(N+2)/8)·v (leaves in singlet s_R=0) gives H · v = 0. Decoupling sector (γ-5 step 321) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1368) |
| singleClusterHamiltonianS_eigenvalue_pentamer_leaf_singlet | Pentamer leaf-singlet sector eigenvalue = 0: for z=4, joint eigenvector at s_tot=N/2 and 6-pair sum (-N(N+2)/2)·v (leaves in singlet s_R=0) gives H · v = 0. Decoupling sector; 4-leaf singlet exists for any S (γ-5 step 322) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1369) |
| singleClusterHamiltonianS_eigenvalue_leaf_singlet | Generic leaf-singlet decoupling (any z): if Stot²·v = (N(N+2)/4)·v (s_tot=N/2) and leafSpinSSquared z N · v = 0 (leaves in singlet), then H · v = 0. Generalises γ-5 steps 296 (z=2), 321 (z=3), 322 (z=4) (γ-5 step 323) | Quantum/SpinS/SingleClusterHamiltonianConcreteClusters.lean (PR #1370) |
| singleClusterHamiltonianS_hermitianMinEigenvalue_le_gs_of_gs_sector / singleClusterHamiltonianS_hermitianMinEigenvalue_le_gs_of_exists_gs_sector | Single-cluster variational upper-bound bridge: a non-zero vector in the predicted GS Casimir sector (s_R = zN/2, s_tot = (z−1)N/2) gives hermitianMinEigenvalue H ≤ Re (singleClusterGSEnergyS z N). The existential form packages the Clebsch–Gordan vector construction as the remaining hypothesis for Problem 2.5.a (γ-5 step 324) | Quantum/SpinS/SingleClusterHamiltonianMinCore.lean (PR #4033) |
| singleClusterGSEnergyS_re_le_hermitianMinEigenvalue_of_global_eigenvalue_lower / singleClusterHamiltonianS_hermitianMinEigenvalue_eq_gs_of_gs_sector_and_global_lower / singleClusterHamiltonianS_hermitianMinEigenvalue_eq_gs_of_exists_gs_sector_and_global_lower | Single-cluster lower-bound and equality bridge: a global lower-bound callback for all non-zero real-energy eigenvectors gives Re (singleClusterGSEnergyS z N) ≤ hermitianMinEigenvalue H; combined with a predicted GS-sector witness (or its existential package) this identifies hermitianMinEigenvalue H = Re (singleClusterGSEnergyS z N). The remaining mathematical work is to prove the lower callback from joint-Casimir spectral exhaustion and the GS-sector witness from Clebsch–Gordan theory (γ-5 step 325) | Quantum/SpinS/SingleClusterHamiltonianMinCore.lean + Quantum/SpinS/SingleClusterHamiltonianMin.lean (PR #4034) |
| singleCluster_global_eigenvalue_lower_of_joint_casimir_energy_lower / singleClusterGSEnergyS_re_le_hermitianMinEigenvalue_of_joint_casimir_energy_lower / singleClusterHamiltonianS_hermitianMinEigenvalue_eq_gs_of_gs_sector_and_joint_lower / singleClusterHamiltonianS_hermitianMinEigenvalue_eq_gs_of_exists_gs_sector_and_joint_lower | Joint-Casimir lower callback bridge: if every non-zero real-energy H-eigenvector admits Ŝ_tot² and Ŝ_R² Casimir eigenvalues whose Casimir energy (α − N(N+2)/4 − β)/2 is at least Re (singleClusterGSEnergyS z N), then the global lower callback, Hermitian-min lower bound, and conditional equality wrappers follow. This narrows the remaining lower-bound proof to joint-Casimir spectral exhaustion plus the sector arithmetic bound (γ-5 step 326) | Quantum/SpinS/SingleClusterHamiltonianMinCore.lean + Quantum/SpinS/SingleClusterHamiltonianMin.lean (PR #4035) |
| singleClusterGSEnergyS_re_le_casimir_energy_of_joint_bounds / singleCluster_global_eigenvalue_lower_of_joint_casimir_bounds / singleClusterGSEnergyS_re_le_hermitianMinEigenvalue_of_joint_casimir_bounds | Joint-Casimir sector arithmetic lower bound: a sector with Re α ≥ ((z−1)N/2)(((z−1)N/2)+1) and Re β ≤ (zN/2)(zN/2+1) has Casimir energy (α − N(N+2)/4 − β)/2 at least Re (singleClusterGSEnergyS z N). The callback forms turn these sector bounds for every non-zero real-energy H-eigenvector into the global lower callback and Hermitian-min lower bound (γ-5 step 327) | Quantum/SpinS/SingleClusterHamiltonianMinCore.lean (PR #4036) |
| singleClusterHamiltonianS_minEigenvalue_eq_gs_of_gs_sector_and_joint_casimir_bounds / singleClusterHamiltonianS_minEigenvalue_eq_gs_of_exists_gs_sector_and_joint_casimir_bounds | Conditional equality from joint-Casimir sector bounds: a concrete or existential predicted GS-sector witness gives the upper bound, while the joint-Casimir sector-bounds callback from γ-5 step 327 gives the reverse inequality. This packages the final conditional Problem 2.5.a endpoint before the remaining Clebsch–Gordan witness and spectral sector-bounds proofs (γ-5 step 328) | Quantum/SpinS/SingleClusterHamiltonianMin.lean (PR #4037) |
| leafSpinSSquared_eq_sublatticeSpinSquaredS_leaf / leafSpinSSquared_eigenvalue_re_le_max / singleCluster_global_eigenvalue_lower_of_joint_casimir_total_lower / singleClusterGSEnergyS_re_le_hermitianMinEigenvalue_of_joint_casimir_total_lower / singleClusterHamiltonianS_minEigenvalue_eq_gs_of_gs_sector_and_joint_casimir_total_lower / singleClusterHamiltonianS_minEigenvalue_eq_gs_of_exists_gs_sector_and_joint_casimir_total_lower | Single-cluster leaf-Casimir spectral maximum bound: the leaf Casimir Ŝ_R² is the sublattice Casimir of {x : Fin (z+1) | x ≠ 0}, whose cardinality is z; hence every Ŝ_R² eigenvalue satisfies Re β ≤ (zN/2)(zN/2+1). The new lower-bound and min-eigenvalue callback forms derive the leaf bound internally, so the remaining lower-bound hypothesis only needs joint Casimir spectral data plus the total-Casimir lower bound Re α ≥ ((z−1)N/2)(((z−1)N/2)+1) (γ-5 step 329) | Quantum/SpinS/SingleClusterLeafCasimirBound.lean, Quantum/SpinS/SingleClusterHamiltonianMinCore.lean + Quantum/SpinS/SingleClusterHamiltonianMin.lean (PR #4038) |
| sublatticeSpinSquaredS_compl_leaf_eq_spinSDot_zero_zero / singleClusterGSEnergyS_re_le_casimir_energy_of_coupled_leaf_sector / singleCluster_global_eigenvalue_lower_of_coupled_leaf_sector / singleClusterGSEnergyS_re_le_hermitianMinEigenvalue_of_coupled_leaf_sector | Single-cluster coupled leaf/center sector energy bridge: for 1 ≤ z, the complement of the leaf sublattice is the singleton center, whose Casimir is the scalar single-site value. Applying the existing Clebsch–Gordan coupled lower bound to the leaf/center partition gives the single-cluster Casimir-energy lower bound from magnetization plus joint total/leaf Casimir sector data. This replaces the too-strong raw all-sector Re α ≥ α_pred design with a sector-energy bridge based on the actual leaf spin parameter (γ-5 step 330) | Quantum/SpinS/SingleClusterCoupledSectorEnergy.lean, Quantum/SpinS/SingleClusterHamiltonianMin.lean (PR #4039) |
| mulVec_magProjFn_eq_of_mulVec_basisVecS_mem_magSubspaceS / singleClusterHamiltonianS_commute_totalSpinSOp3 / singleClusterHamiltonianS_mulVec_mem_magSubspaceS_of_mem / singleClusterHamiltonianS_mulVec_basisVecS_mem_magSubspaceS / singleClusterHamiltonianS_mulVec_magProjFn_eq / singleClusterHamiltonianS_eigenvec_exists_weight_component | Single-cluster magnetization projection bridge: the single-cluster Hamiltonian commutes with total magnetization, preserves each magSubspaceS, and commutes with the pointwise magnetization projections magProjFn via the generic basis-vector preservation helper. Hence every non-zero single-cluster Hamiltonian eigenvector has a non-zero magnetization component that is again an eigenvector with the same energy. This supplies the magnetization-extraction layer for the remaining joint total/leaf Casimir sector-decomposition route (γ-5 step 331) | Quantum/SpinS/SingleClusterMagnetizationProjection.lean (PR #4040) |
| exists_eigenvector_in_invariant_submodule | Invariant-submodule eigenvector bridge: over an algebraically closed field, any non-zero finite-dimensional submodule invariant under an endomorphism contains a non-zero eigenvector of that endomorphism. The proof restricts the endomorphism to the submodule and applies Mathlib’s finite-dimensional eigenvalue-existence theorem. This is the linear-algebra bridge for the next Problem 2.5.a joint total/leaf Casimir sector-decomposition step after magnetization extraction (γ-5 step 332) | Math/InvariantSubmoduleEigenvector.lean (PR #4041) |
| exists_joint_eigenvector_in_invariant_submodule | Joint invariant-submodule eigenvector bridge: over an algebraically closed field, any non-zero finite-dimensional submodule invariant under two commuting endomorphisms contains a non-zero simultaneous eigenvector for both. The proof first extracts an eigenvector for the first endomorphism, then applies the one-operator bridge to the non-zero intersection of the original submodule with that eigenspace, using commutativity to prove invariance under the second endomorphism. This packages the next linear-algebra step for extracting total/leaf Casimir sector data inside the single-cluster magnetization/Hamiltonian component (γ-5 step 333) | Math/InvariantSubmoduleEigenvector.lean (PR #4042) |
| singleCluster_totalSpinSSquared_commute_leafSpinSSquared / singleClusterHamiltonianS_commute_totalSpinSSquared / singleClusterHamiltonianS_commute_leafSpinSSquared / singleClusterHamiltonianMagEigenspaceSubmodule / singleCluster_totalSpinSSquared_mulVecLin_commute_leafSpinSSquared_mulVecLin / singleClusterHamiltonianMagEigenspaceSubmodule_totalSpinSSquared_invariant / singleClusterHamiltonianMagEigenspaceSubmodule_leafSpinSSquared_invariant / exists_joint_casimir_eigenvector_in_singleClusterHamiltonianMagEigenspaceSubmodule | Single-cluster Casimir invariance bridge: the Casimir decomposition (2 : ℂ) • H = (Ŝ_tot)² - Ŝ_0² - Ŝ_R², the scalar central-site Casimir, and the total/leaf sublattice-Casimir commutation theorem show that the single-cluster Hamiltonian commutes with both the total and leaf Casimirs. Consequently the Hamiltonian eigenspace intersected with a fixed magnetization subspace is invariant under both Casimirs, and any non-zero such submodule contains a non-zero joint total/leaf Casimir eigenvector when the caller supplies the explicit algebraically closed field hypothesis [IsAlgClosed ℂ] (γ-5 step 334) | Quantum/SpinS/SingleClusterCasimirInvariance.lean (PR #4043) |
| singleCluster_global_eigenvalue_lower_of_exists_joint_casimir_energy_lower / singleClusterGSEnergyS_re_le_hermitianMinEigenvalue_of_exists_joint_casimir_energy_lower / singleClusterHamiltonianS_hermitianMinEigenvalue_eq_gs_of_gs_sector_and_exists_joint_lower / singleClusterHamiltonianS_minEigenvalue_eq_gs_of_exists_gs_sector_and_exists_joint_lower | Same-energy joint-Casimir lower bridge: the lower-bound callback no longer needs the original non-zero real-energy H-eigenvector to be a joint total/leaf Casimir eigenvector. It is enough to produce a non-zero same-energy witness w whose total/leaf Casimir eigenvalues have Casimir energy at least Re (singleClusterGSEnergyS z N). The proof identifies the common energy by applying the existing joint-Casimir Hamiltonian eigenvalue theorem to w and cancelling scalar multiplication by the non-zero witness; Hermitian-min lower and conditional equality wrappers follow (γ-5 step 335) | Quantum/SpinS/SingleClusterHamiltonianMinCore.lean + Quantum/SpinS/SingleClusterHamiltonianMin.lean (PR #4044) |
| singleCluster_exists_joint_casimir_energy_lower_of_mag_component_joint_lower / singleClusterGSEnergyS_re_le_hermitianMinEigenvalue_of_mag_component_joint_lower / singleClusterHamiltonianS_minEigenvalue_eq_gs_of_gs_sector_and_mag_joint_lower / singleClusterHamiltonianS_minEigenvalue_eq_gs_of_exists_gs_sector_and_mag_joint_lower | Single-cluster joint-Casimir witness bridge: magnetization extraction turns any non-zero real-energy Hamiltonian eigenvector into a non-zero same-energy magnetization component. This proves the corresponding Hamiltonian/magnetization submodule is non-zero; the invariant-submodule Casimir theorem then supplies a non-zero same-energy joint total/leaf Casimir eigenvector in that submodule. A remaining Casimir-energy lower callback on such extracted joint vectors therefore yields the same-energy witness callback from PR #4044, plus Hermitian-min lower and conditional equality wrappers under the explicit [IsAlgClosed ℂ] hypothesis (γ-5 step 336) | Quantum/SpinS/SingleClusterJointCasimirWitness.lean (PR #4045) |
| singleCluster_mag_component_joint_lower_of_coupled_leaf_sector / singleClusterGSEnergyS_re_le_hermitianMinEigenvalue_of_extracted_coupled_leaf_sector / singleClusterHamiltonianS_minEigenvalue_eq_gs_of_gs_sector_and_extracted_coupled_leaf_sector / singleClusterHamiltonianS_minEigenvalue_eq_gs_of_exists_gs_sector_and_extracted_coupled | Extracted coupled leaf-sector lower bridge: for 1 ≤ z, any non-zero joint total/leaf Casimir vector in an extracted Hamiltonian/magnetization submodule has an attained magnetization value. Reindexing M = m_max − magSumS σ as M = k − m_max lets the existing coupled leaf/center sector-energy theorem supply the Casimir-energy lower callback required by PR #4045. This gives the Hermitian-min lower bound and conditional equality wrappers under [IsAlgClosed ℂ] (γ-5 step 337) | Quantum/SpinS/SingleClusterExtractedCoupledLower.lean (PR #4046) |
| singleCluster_exists_gs_joint_casimir_witness / singleClusterHamiltonianS_minEigenvalue_eq_gs_of_predicted_joint_witness | Single-cluster predicted GS joint-Casimir witness and final equality wrapper: for 1 ≤ z, specialize the existing bipartite predicted joint-Casimir eigenvector to the leaf/center split of Fin (z+1). The leaf set has cardinality z and the center complement has cardinality 1, so the witness has total Casimir ((z−1)N/2)(((z−1)N/2)+1) and leaf Casimir (zN/2)(zN/2+1). Feeding this witness into the extracted coupled lower bridge identifies hermitianMinEigenvalue H = Re (singleClusterGSEnergyS z N) under [IsAlgClosed ℂ] (γ-5 step 338) | Quantum/SpinS/SingleClusterGSJointWitness.lean (PR #4047) |
| Matrix.isHermitian_sum / rayleighOnVec_sum_matrix / sum_lower_bounds_le_hermitianMinEigenvalue_sum / add_lower_bounds_le_hermitianMinEigenvalue_add / tasaki25b_local_cluster_sum_lower_bound / tasaki25b_local_cluster_sum_lower_bound_closed_form | Problem 2.5.b sum lower-bound bridge: packages Tasaki’s Lemma A.5 argument for finite-dimensional Hermitian matrices. If each local Hamiltonian has a lower bound ε x, then the Hermitian minimum eigenvalue of the sum is at least Σ x, ε x. The local-cluster wrappers specialize this to the Problem 2.5.a star-cluster energies, yielding the abstract lower bound E_GS ≥ -Σ_{x∈A} S(1 + degree(x) S) with S = N/2 once a graph Hamiltonian is decomposed into centered local cluster terms (γ-6 step 339). The generic “a finite sum of Hermitian matrices is Hermitian” helper has been extracted as Matrix.isHermitian_sum into Math/MatrixAnalysis/HermitianSum.lean (PR #4341), replacing the per-file private copies in Quantum/IsingChain.lean, Quantum/TotalSpin.lean, and Quantum/SpinS/TotalSpin.lean | Quantum/SpinS/HermitianMinEigenvalueSumLower.lean (PR #4048), Math/MatrixAnalysis/HermitianSum.lean (PR #4341) |
| graphLocalClusterHamiltonianS / graphLocalClusterHamiltonianS_isHermitian / heisenbergHamiltonianOnGraphS_one_eq_sum_graphLocalClusterHamiltonianS / heisenbergHamiltonianOnGraphS_half_eq_sum_filter_graphLocalClusterHamiltonianS | Problem 2.5.b graph-local decomposition: defines the same-Hilbert-space local star Hamiltonian h_x = Σ_{y∈N_G(x)} Ŝ_x · Ŝ_y. The unit-coupling graph Hamiltonian is Σ_x h_x under the repository’s ordered-pair convention, and on a bipartite graph the half-coupling Hamiltonian is the one-sided sum Σ_{x∈A} h_x, using the pair swap and spinSDot_comm. This pins the coefficient convention needed before applying the Problem 2.5.a local-cluster lower bounds (γ-6 step 340) | Quantum/SpinS/HeisenbergGraphLocal.lean (PR #4050) |
| siteConfigEquiv / siteConfigEquiv_apply / siteConfigEquiv_symm_apply / reindex_onSiteS_siteEquiv / reindex_spinSDot_siteEquiv / transportedSingleClusterHamiltonianS / transportedSingleClusterHamiltonianS_eq_sum / optionClusterHamiltonianS / singleClusterOptionEquiv / sum_fin_erase_zero_eq_sum_succ / transportedSingleClusterHamiltonianS_option_eq | Problem 2.5.b single-cluster transport bridge: transports many-body spin operators along an equivalence of site types. A transported singleClusterHamiltonianS z N is the sum of dot products between the transported center and leaves; in particular, the canonical Fin (s.card + 1) ≃ Option s equivalence turns the abstract single-cluster Hamiltonian into the option-star Hamiltonian with center none and leaves some y. This isolates the reindexing part of the remaining graph-local-star comparison (γ-6 step 341) | Quantum/SpinS/SingleClusterTransport.lean (PR #4051) |
| graphLocalStarConfig / graphLocalStarConfig_center / graphLocalStarConfig_neighbor / graphLocalStarConfig_outside / graphLocalStarConfig_agree_off_pair_of_option_agree / option_agree_of_graphLocalStarConfig_agree_off_pair / spinSDot_graphLocalStarConfig_eq_option / graphLocalClusterHamiltonianS_apply_eq_zero_of_outside_diff / graphLocalClusterHamiltonianS_block_eq_optionClusterHamiltonianS | Problem 2.5.b graph-local star block bridge: fixes an outside configuration and embeds option-star configurations into the full graph Hilbert space. The graph-local star has zero matrix entries between configurations with different outside restrictions, and each fixed-outside block is exactly the option-star Hamiltonian on Option (G.neighborFinset x). This supplies the same-Hilbert-space block comparison needed before turning the Problem 2.5.a local-cluster bound into a full graph-local lower bound (γ-6 step 342) | Quantum/SpinS/GraphLocalStarBlockCore.lean (embedding + matrix-entry comparison) + Quantum/SpinS/GraphLocalStarBlock.lean (block identity, split for build speed) (PR #4052) |
| graphLocalOutsideSite / graphLocalOutsideSite_fintype / graphLocalOutsideSite_decidableEq / graphLocalOutsideConfigExtend / graphLocalProductConfig / graphLocalConfigEquiv / graphLocalConfigEquiv_apply_none / graphLocalConfigEquiv_apply_some / graphLocalConfigEquiv_apply_outside / graphLocalConfigEquiv_symm_apply / graphLocalProductConfig_outside / graphLocalClusterHamiltonianS_product / graphLocalClusterHamiltonianS_product_isHermitian / graphLocalClusterHamiltonianS_product_apply_of_outside_eq / graphLocalClusterHamiltonianS_product_apply_of_outside_ne / graphLocalClusterHamiltonianS_product_mulVec / matrix_mulVec_reindex_comp_symm / dotProduct_comp_equiv_symm / rayleighOnVec_reindex_comp_symm / dotProduct_product_re_eq_sum_blocks / rayleighOnVec_graphLocalClusterHamiltonianS_product / graphLocalClusterHamiltonianS_product_rayleigh_lower / graphLocalClusterHamiltonianS_product_minEigenvalue_lower / graphLocalClusterHamiltonianS_rayleigh_lower / graphLocalClusterHamiltonianS_minEigenvalue_lower | Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/GraphLocalStarLowerBoundCore.lean (product coordinates + product cluster Hamiltonian with Hermiticity / outside-block apply) + Quantum/SpinS/GraphLocalStarLowerBound.lean (product mulVec + reindexing + Rayleigh decomposition over outside blocks + lower bound, split for build speed) (PR #4053) |
| transportedSingleClusterHamiltonianS_isHermitian / optionClusterHamiltonianS_isHermitian / dotProduct_comp_equiv / rayleighOnVec_reindex_comp / optionClusterHamiltonianS_rayleigh_lower_singleClusterGSEnergy / graphLocalClusterHamiltonianS_minEigenvalue_lower_singleClusterGSEnergy / tasaki25b_graphLocalCluster_sum_lower_bound / tasaki25b_heisenbergHamiltonianOnGraphS_half_lower_bound | Problem 2.5.b option-star and graph-local sum wrapper: transports the Problem 2.5.a minimum-eigenvalue formula to the canonical option-star Hamiltonian by Rayleigh reindexing. Under [IsAlgClosed ℂ] and the local positive-degree hypothesis 1 ≤ (G.neighborFinset x).card, this gives the single-cluster ground-energy lower bound for the same-Hilbert-space graph-local star. The finite-sum wrapper then bounds a chosen family of graph-local stars, and the bipartite half-coupling theorem applies the bound directly to heisenbergHamiltonianOnGraphS G (1 / 2) N = Σ_{x∈A} h_x for one side of a bipartition (γ-6 step 344) | Quantum/SpinS/GraphLocalStarSumWrapper.lean (PR #4054) |
| tasaki25b_graphLocalCluster_sum_lower_bound_closed_form / tasaki25b_graphLocalCluster_sum_lower_bound_degree_closed_form / tasaki25b_heisenbergHamiltonianOnGraphS_half_lower_bound_closed_form / tasaki25b_heisenbergHamiltonianOnGraphS_half_lower_bound_degree_closed_form | Problem 2.5.b closed-form and degree wrappers: rewrites the graph-local star and half-coupling graph-Hamiltonian lower bounds using the explicit Problem 2.5.a formula Re E_GS(z) = -(N/2)(zN/2+1). The degree-spelled variants replace (G.neighborFinset x).card by G.degree x, matching Tasaki’s graph-theoretic statement while preserving the necessary positive-degree hypothesis for centers on the chosen side (γ-6 step 345) | Quantum/SpinS/GraphLocalStarSumWrapper.lean (PR #4055) |
| totalSpinSSquared_eq_diag_plus_offdiag / totalSpinSSquared_eq_constMul_one_plus_offdiag / sum_offdiag_spinSDot_fin_two / totalSpinSSquared_fin_two / two_smul_spinSDot_fin_two / spinSDot_fin_two_eq | Multi-site Casimir decomposition and its two-site specialisation (Tasaki Problem 2.5.a, single-bond z = 1 case): the diagonal/off-diagonal split (Ŝ_tot)² = Σ_x Ŝ_x · Ŝ_x + Σ_{x ≠ y} Ŝ_x · Ŝ_y, its per-site-Casimir-substituted form (Ŝ_tot)² = (\|Λ\|·N(N+2)/4) • 1 + Σ_{x ≠ y} Ŝ_x · Ŝ_y, and for Λ = Fin 2 the collapse of the off-diagonal sum to 2 • (Ŝ_0 · Ŝ_1) by spinSDot_comm, giving (Ŝ_tot)² = (N(N+2)/2) • 1 + 2 • (Ŝ_0 · Ŝ_1) and its solved forms 2 • (Ŝ_0 · Ŝ_1) = (Ŝ_tot)² − (N(N+2)/2) • 1 and Ŝ_0 · Ŝ_1 = (1/2) • (Ŝ_tot)² − (N(N+2)/4) • 1 | Quantum/SpinS/MultiSiteCasimirCore.lean (wired into the build root by PR #5146) |
| spinSDot_fin_two_mulVec_of_totalSpinSSquared_eigenvec / smul_spinSDot_fin_two_mulVec_of_totalSpinSSquared_eigenvec / spinSDot_fin_two_mulVec_of_totalSpinSSquared_zero | Two-site Casimir-to-bond eigenvalue conversion (Tasaki Problem 2.5.a, single-bond z = 1 case): on Fin 2, every (Ŝ_tot)²-eigenvector at λ is an Ŝ_0 · Ŝ_1-eigenvector at λ/2 − N(N+2)/4, hence a J • (Ŝ_0 · Ŝ_1)-eigenvector at J·(λ/2 − N(N+2)/4) for any coupling J : ℂ; the singlet specialisation λ = 0 gives eigenvalue −N(N+2)/4 = −S(S+1). These are operator-level eigenvalue conversions: they identify the bond eigenvalue in each (Ŝ_tot)² sector and do not by themselves prove that −S(S+1) is the minimum (the variational side is the singleCluster* chain above). Overlap note: the first and third are an alternative spelling of singleClusterHamiltonianS_eigenvalue_dimer / singleClusterHamiltonianS_eigenvalue_dimer_singlet (γ-5 steps 286/287, already listed above in this table), because singleClusterHamiltonianS 1 N = spinSDot 0 1 N on Fin 2 and (α − N(N+2)/2)/2 = α/2 − N(N+2)/4; each of those two pairs was machine-checked to derive from the other in four lines, so consolidating them is a #5098 follow-up and this row records the overlap rather than a new result | Quantum/SpinS/MultiSiteCasimir.lean (wired into the build root by PR #5146) |
| totalSpinHalfOp{1,2,3}_eq_sublattice_sum | total spin decomposition: Ŝ_tot^(α) = Ŝ_A^(α) + Ŝ_¬A^(α) for α ∈ {1, 2, 3}. Direct from the partition Λ = A ∪ ¬A | Quantum/MarshallLiebMattis/SublatticeSpinCore.lean |
| sublatticeSpinHalfSquared / sublatticeSpinHalfSquared_isHermitian | sublattice spin Casimir: (Ŝ_A)² := Σ_α (Ŝ_A^(α))². Hermitian (each (Ŝ_A^(α))² is the square of a Hermitian operator). Foundation for the Casimir identity Ĥ_toy = (1/(2|Λ|))((Ŝ_tot)² − (Ŝ_A)² − (Ŝ_B)²) (Tasaki §2.5 (2.5.11)) | Quantum/MarshallLiebMattis/SublatticeSpinCore.lean |
| sublatticeSpinHalfOpGeneric_cross_commute / sublatticeSpinHalfOp{1,2,3}_cross_commute_op{1,2,3} | mixed-axes cross-sublattice commutativity: Commute (Ŝ_A^(α)) (Ŝ_¬A^(β)) for any axes α, β ∈ {1, 2, 3}. Generic helper expresses this for arbitrary single-site operators S, T; the six mixed-axis specialisations follow as one-line corollaries | Quantum/MarshallLiebMattis/SublatticeSpinCore.lean |
| sublatticeSpinHalfSquared_cross_commute | the two sublattice Casimirs commute: Commute (Ŝ_A)² (Ŝ_¬A)². Each pairwise component Commute ((Ŝ_A^(α))²) ((Ŝ_¬A^(β))²) follows from the mixed-axes cross-commute by chaining Commute.mul_left / mul_right. Sets up the joint eigenbasis of (Ŝ_tot)², (Ŝ_A)², (Ŝ_¬A)² for the toy-Hamiltonian eigenvalue analysis | Quantum/MarshallLiebMattis/SublatticeSpinCore.lean |
| sublatticeSpinHalfOp{1,2,3}_commutator_sublatticeSpinHalfOp{2,3,1} | Sublattice SU(2) algebra: [Ŝ_A^(α), Ŝ_A^(β)] = i ε^αβγ Ŝ_A^(γ) for each cyclic axis triple. Generic helper sublatticeSpin_commutator_general lifts the single-site commutator [Sα, Sβ] = i • Sγ to the sublattice sum (off-diagonal pairs vanish by onSite_mul_onSite_of_ne; diagonal contributes if A x then i • onSite x Sγ else 0) | Quantum/MarshallLiebMattis/SublatticeSpinCore.lean |
| sublatticeSpinHalfSquared_commute_sublatticeSpinHalfOp{1,2,3} | Sublattice Casimir self-invariance: Commute (Ŝ_A)² (Ŝ_A^(α)) for each axis. Standard SU(2) Casimir argument applied at the sublattice level: per-axis Leibniz rule [X², C] = X[X,C] + [X,C]X combined with the sublattice SU(2) algebra. Together with cross-commute, gives Commute (Ŝ_A)² (Ŝ_tot^(α)), hence Commute (Ŝ_A)² (Ŝ_tot)² | Quantum/MarshallLiebMattis/SublatticeSpinCore.lean |
| sublatticeSpinHalfSquared_commute_sublatticeSpinHalfOp{1,2,3}_complement / _totalSpinHalfOp{1,2,3} / _totalSpinHalfSquared | (Ŝ_A)² commutes with each Ŝ_¬A^(α) (Commute.mul_left over the mixed-axes cross-commute), with each Ŝ_tot^(α) = Ŝ_A^(α) + Ŝ_¬A^(α), and with (Ŝ_tot)² = Σ_α (Ŝ_tot^(α))². Provides the third pairwise commutativity needed for the joint eigenbasis of (Ŝ_tot)², (Ŝ_A)², (Ŝ_¬A)² (the first two are α-6r self-invariance and α-6o inter-Casimir cross-commute) | Quantum/MarshallLiebMattis/SublatticeSpinCore.lean |
| sublatticeSpinDot / sublatticeSpinDot_complement_isHermitian | cross-sublattice spin dot product: Ŝ_A · Ŝ_B := Σ_α Ŝ_A^(α) Ŝ_B^(α). Ŝ_A · Ŝ_¬A is Hermitian (each summand is the product of two commuting Hermitian operators). Bilinear expansion sublatticeSpinDot_eq_sum_sum: Ŝ_A · Ŝ_B = Σ_{x : A x} Σ_{y : B y} Ŝ_x · Ŝ_y connects the operator-level Casimir form to the bond-level Heisenberg expression in the toy Hamiltonian (Tasaki §2.5 (2.5.10)) | Quantum/MarshallLiebMattis/SublatticeSpinDot.lean |
| sublatticeSpinHalfSquared_eq_sum_dot / sublatticeSpinHalfSquared_mulVec_basisVec_const / _all_up / _all_down / _of_const_on | (Ŝ_A)² = Σ_{x ∈ A} Σ_{y ∈ A} Ŝ_x · Ŝ_y (specialisation B = A of the bilinear expansion), and the maximum-spin Casimir eigenvalue on the all-aligned state: (Ŝ_A)² · \|s s … s⟩ = (\|A\|·(\|A\|+2)/4) · \|s s … s⟩ for any s : Fin 2. Generalised form _of_const_on: any \|σ⟩ with σ constant on A is an eigenvector with eigenvalue \|A\|·(\|A\|+2)/4 (relevant for Néel-style states which are constant on each sublattice but not globally) | Quantum/MarshallLiebMattis/SublatticeSpinDot.lean |
| heisenbergToyHamiltonian_eq_sublatticeSpinDot_sum | the MLM toy Hamiltonian decomposes as an oriented cross-sublattice spin dot product: Ĥ_toy = Ŝ_A · Ŝ_¬A + Ŝ_¬A · Ŝ_A. Bridges the bipartite-bond sum (Tasaki §2.5 (2.5.10)) to the operator-level Casimir form (Tasaki §2.5 (2.5.11)) | Quantum/MarshallLiebMattis/ToyHamiltonianCasimir.lean |
| sublatticeSpinDot_complement_comm / heisenbergToyHamiltonian_eq_two_sublatticeSpinDot | cross-sublattice symmetry: Ŝ_A · Ŝ_¬A = Ŝ_¬A · Ŝ_A (each axis pair commutes by sublatticeSpinHalfOp{1,2,3}_cross_commute), giving the closed form Ĥ_toy = 2 • Ŝ_A · Ŝ_¬A | Quantum/MarshallLiebMattis/ToyHamiltonianCasimir.lean |
| totalSpinHalfSquared_eq_sublattice_casimir / heisenbergToyHamiltonian_eq_casimir_diff | Casimir identity (Tasaki §2.5 (2.5.11)): (Ŝ_tot)² = (Ŝ_A)² + 2 • (Ŝ_A · Ŝ_¬A) + (Ŝ_¬A)² (per-axis (a + b)² = a² + 2ab + b² via cross-commute), and the closed form (without 1/|Λ|) Ĥ_toy = (Ŝ_tot)² − (Ŝ_A)² − (Ŝ_¬A)² | Quantum/MarshallLiebMattis/ToyHamiltonianCasimir.lean |
| heisenbergToyHamiltonian_commute_totalSpinHalfSquared | the toy Hamiltonian commutes with (Ŝ_tot)² (specialisation of heisenbergHamiltonian_commute_totalSpinHalfSquared). The standard fact used to project the toy ground state onto a fixed (Ŝ_tot)² eigenspace, underpinning the S_tot = 0 selection of the toy ground state | Quantum/MarshallLiebMattis/ToyHamiltonianCasimir.lean |
| heisenbergToyHamiltonian_commute_sublatticeSpinHalfSquared / _complement | the toy Hamiltonian commutes with (Ŝ_A)² and with (Ŝ_¬A)². Direct consequences of the closed form Ĥ_toy = (Ŝ_tot)² − (Ŝ_A)² − (Ŝ_¬A)² and the three pairwise Casimir commutativities (PRs α-6o, α-6s, self-commute trivially). Together with α-6p, gives all four Casimir-style commutators of Ĥ_toy, the prerequisite for the joint eigenbasis analysis on which the S_tot = 0 selection rests | Quantum/MarshallLiebMattis/ToyHamiltonianCasimir.lean |
| heisenbergToyHamiltonian_mulVec_basisVec_const / _simplified | explicit eigenvalue of Ĥ_toy on the all-aligned state: the Casimir-difference form \|Λ\|·(\|Λ\|+2)/4 − \|A\|·(\|A\|+2)/4 − \|¬A\|·(\|¬A\|+2)/4 algebraically simplifies via \|Λ\| = \|A\| + \|¬A\| to the product form \|A\|·\|¬A\|/2. The eigenvalue is non-negative for any bipartite lattice and strictly positive when both sublattices are non-empty | Quantum/MarshallLiebMattis/ToyHamiltonianCasimir.lean |
| sublatticeSpinHalfSquared_mulVec_neelStateOf / _complement_mulVec_neelStateOf | sublattice Casimir eigenvalues on the Néel state Φ_Néel(A) := basisVec (neelConfigOf A): (Ŝ_A)² · \|Φ_Néel(A)⟩ = (\|A\|·(\|A\|+2)/4) · \|Φ_Néel(A)⟩ and (Ŝ_¬A)² · \|Φ_Néel(A)⟩ = (\|¬A\|·(\|¬A\|+2)/4) · \|Φ_Néel(A)⟩. Direct corollaries of _of_const_on since the Néel configuration is constant on each sublattice (σ x = 0 on A, σ x = 1 on ¬A); the Néel state is simultaneously a (Ŝ_A)² and (Ŝ_¬A)² eigenvector at maximum-spin eigenvalues | Quantum/MarshallLiebMattis/SublatticeCasimirNeelCore.lean |
| mulVec_mem_magnetizationSubspace_of_commute_of_mem | generic preservation: any operator A with Commute A (Ŝtot^(3)) maps each magnetisation sector H_M to itself — operator-level form of Tasaki §2.2 (2.2.10), p. 22 block-diagonalisation | Quantum/MagnetizationSubspace.lean |
| totalSpinHalfSquared_mulVec_mem_magnetizationSubspace_of_mem | Casimir specialisation: Ŝtot² preserves every H_M (since [Ŝtot², Ŝtot^(3)] = 0) | Quantum/MagnetizationSubspace.lean |
| heisenbergHamiltonian_mulVec_mem_magnetizationSubspace_of_mem | for any J : Λ → Λ → ℂ and M : ℂ, v ∈ H_M implies H · v ∈ H_M — the operator-level statement that any Heisenberg Hamiltonian block-diagonalises against Tasaki §2.2 (2.2.10), p. 22 magnetisation-sector decomposition (consequence of SU(2) invariance [H, Ŝtot^(3)] = 0) | Quantum/MagnetizationSubspace.lean |
| totalSpinHalfOpMinus_mulVec_mem_magnetizationSubspace_of_mem | for any M : ℂ, v ∈ H_M implies Ŝtot^- · v ∈ H_{M-1} — the standard SU(2) lowering ladder action via the Cartan relation [Ŝtot^(3), Ŝtot^-] = -Ŝtot^- | Quantum/MagnetizationSubspace.lean |
| totalSpinHalfOpPlus_mulVec_mem_magnetizationSubspace_of_mem | for any M : ℂ, v ∈ H_M implies Ŝtot^+ · v ∈ H_{M+1} — the SU(2) raising ladder action via [Ŝtot^(3), Ŝtot^+] = +Ŝtot^+ | Quantum/MagnetizationSubspace.lean |
| totalSpinHalfRot{1,2,3}_two_site | for Λ = Fin 2 and any θ, the global rotation factors as onSite 0 (Û^(α)_θ) * onSite 1 (Û^(α)_θ) (general-θ extension of Problem 2.2.b) | Quantum/TotalSpin/Rotation.lean |
| onSite_exp_eq_exp_onSite | onSite x (exp A) = exp (onSite x A) — bridge between single-site and many-body matrix exponential. Local Frobenius normed structure + LinearMap.continuous_of_finiteDimensional + NormedSpace.map_exp | Quantum/TotalSpin/Rotation.lean |
| totalSpinHalfRot{1,2,3}_eq_exp | Tasaki eq. (2.2.11): Û^(α)_θ_tot = exp(-iθ Ŝ_tot^(α)). Composes spinHalfRot{α}_eq_exp (single site), onSite_exp_eq_exp_onSite (per-site bridge), and Matrix.exp_sum_of_commute (commuting-summand exp = noncommProd of exps) | Quantum/TotalSpin/Rotation.lean |
| totalSpinHalfRot{1,2,3}_commute_of_commute | Tasaki §2.2 (2.2.12) → (2.2.13): Commute A (Ŝ_tot^(α)) → Commute A (Û^(α)_θ_tot). Generic operator version, follows from Commute.exp_right after rewriting Û via _eq_exp | Quantum/TotalSpin/Rotation.lean |
| totalSpinHalfOp{Plus,Minus}_exp_commute_of_commute | ladder version: Commute A (Ŝ^±_tot) → Commute A (exp(c • Ŝ^±_tot)) for any c : ℂ (useful for U(1) symmetry) | Quantum/TotalSpin/Rotation.lean |
| totalSpinHalfRot{1,2,3}_conjTranspose_mul_self | (Û^(α)_θ_tot)ᴴ * Û^(α)_θ_tot = 1 (unitarity). Derived from exp_mem_unitary_of_mem_skewAdjoint after recognizing -iθ Ŝ_tot^(α) as skew-adjoint | Quantum/TotalSpin/Rotation.lean |
| totalSpinHalfRot{1,2,3}_conj_eq_self_of_commute | Tasaki eq. (2.2.13) finite form: Commute A (Ŝ_tot^(α)) → (Û^(α)_θ_tot)ᴴ * A * Û^(α)_θ_tot = A. Combines _commute_of_commute with unitarity | Quantum/TotalSpin/Rotation.lean |
| IsInMagnetizationSubspace | predicate for the magnetization-M eigenspace H_M (Tasaki eq. (2.2.9)/(2.2.10)) | Quantum/MagnetizationSubspaceCore.lean |
| magnetizationSubspace M | the magnetization-M eigenspace as a Submodule ℂ ((Λ → Fin 2) → ℂ) | Quantum/MagnetizationSubspaceCore.lean |
| basisVec_mem_magnetizationSubspace | |σ⟩ ∈ H_{|σ|/2} — basis states lie in their magnetization subspace | Quantum/MagnetizationSubspaceCore.lean |
| magnetizationSubspace_disjoint | distinct sectors H_M ⊓ H_{M'} = ⊥ (M ≠ M') — eigenvalue uniqueness | Quantum/MagnetizationSubspaceCore.lean |
| iSup_magnetizationSubspace_eq_top | ⨆_M H_M = ⊤ — every vector decomposes as a sum across sectors | Quantum/MagnetizationSubspaceCore.lean |
| magnetizationSubspace_eq_eigenspace | bridge H_M = (Ŝ_tot^(3) as End).eigenspace M (used to inherit iSupIndep) | Quantum/MagnetizationSubspaceCore.lean |
| magnetizationSubspace_iSupIndep | iSupIndep: each sector is disjoint from the supremum of all others | Quantum/MagnetizationSubspaceCore.lean |
| magnetizationSubspace_isInternal | DirectSum.IsInternal: full direct-sum decomposition H = ⊕_M H_M (Tasaki eqs. (2.2.9)/(2.2.10)) | Quantum/MagnetizationSubspaceCore.lean |
← Total spin operator (Tasaki §2.2 eq. (2.2.7), (2.2.8)) · Catalogue · Two-site spin inner product (Tasaki §2.2 eq. (2.2.16)) →