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 models, Chapters 3–7, and spectral tools
| Lean name | Statement | File |
|---|---|---|
afmHeisenbergChainHamiltonianS / haldaneConjecture |
§6.1 Haldane “conjecture” (def : Prop, never asserted true; eqs. (6.1.1)–(6.1.3)): the 1D AFM Heisenberg chain Ĥ = Σ_x Ŝ_x·Ŝ_{x+1} (PBC, ringCoupling, eq. 6.1.1, spin S=N/2). The spectral-gap dichotomy is captured by realSpectrum (real eigenvalues), IsGroundEnergy, IsPositiveSpectralGap (first excited − ground), GapOfChain, IsGapless (gap → 0 as L↑∞, the O(1/L) half-integer case), IsGapped (∃ uniform Haldane gap Δ>0). haldaneConjecture N := (Odd N → IsGapless N) ∧ (2 ≤ N → Even N → IsGapped N): half-odd-integer S (N odd) gapless, integer S (N even ≥ 2) gapped. A conjecture recorded as a Prop only (never proven/asserted); the correlation-decay clauses (HOI3)/(I3) are deferred. Opens Tasaki Chapter 6 (Part II, Haldane phenomena) |
Quantum/SpinS/HaldaneConjecture.lean |
lsmTwistOperator / lsm_energy_bound / lsm_ground_twist_orthogonal / lieb_schultz_mattis_affleck_lieb |
Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/LiebSchultzMattis.lean, Quantum/SpinS/LiebSchultzMattisRingGap.lean, Quantum/SpinS/LiebSchultzMattisProof.lean, Quantum/SpinS/LiebSchultzMattisOrthogonality.lean |
hermitian_second_eigenvalue_variational |
§6.2 Theorem 6.3 / Courant–Fischer (HermitianSecondEigenvalue.lean, toward Theorem 6.3): the generic finite-dim second-eigenvalue variational bound — for a Hermitian M with a one-dimensional E₀-eigenspace spanned by φ₀ (M φ₀ = E₀ φ₀) and a real E₁ lower-bounding every eigenvalue ≠ E₀, every ψ ⊥ φ₀ satisfies E₁ · ‖ψ‖² ≤ rayleighOnVec M ψ (eigenbasis expansion via spectral_theorem; orthogonality to φ₀ annihilates the E₀ components since the ground line is 1-dim). The Courant–Fischer step assembling the LSM first-excited gap (PR #4849) |
Quantum/SpinS/HermitianSecondEigenvalue.lean |
eigenvalues_mem_realSpectrum / exists_isPositiveSpectralGap |
§6.2 Theorem 6.3 / first excited eigenvalue (ManyBodySpectralGap.lean, toward Theorem 6.3): the model-free spectral core shared by the gap arguments, stated for an arbitrary chain operator H : ManyBodyOpS (Fin L) N (no model, spin value or chain length fixed). eigenvalues_mem_realSpectrum: every Hermitian eigenvalue hH.eigenvalues i lies in realSpectrum H, witnessed by the corresponding member of the eigenvector basis (Matrix.IsHermitian.eigenvectorBasis, nonzero by orthonormality). exists_isPositiveSpectralGap: for a Hermitian H with ground energy E₀ and some spectral point strictly above E₀, the Finset.min' of the eigenvalues above E₀ is a least such point E₁, delivering E₁ ∈ realSpectrum H, E₀ < E₁, the minimality ∀ E ∈ realSpectrum H, E₀ < E → E₁ ≤ E and hence IsPositiveSpectralGap H (E₁ − E₀); internally it uses the private converse bridge exists_eigenvalues_eq_of_mem_realSpectrum (every real-spectrum point is a Hermitian eigenvalue, via Matrix.spectrum_toLin' and Matrix.IsHermitian.spectrum_real_eq_range_eigenvalues). These replace the two private specialisations and the inline Finset.filter/image/min' block that LiebSchultzMattisRingGap.lean previously carried (160 → 111 lines); the ring proof now consumes them and bridges the spectrum-form minimality back to the eigenvalue-index form that hermitian_second_eigenvalue_variational needs. Infrastructure only: no textbook statement changes, lieb_schultz_mattis_affleck_lieb keeps its statement and its std3 axiom profile (PR #5097) |
Quantum/SpinS/ManyBodySpectralGap.lean |
IsShortRangeU1Chain / tasaki_lemma_6_4_general_trial_energy_bound |
Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/LiebSchultzMattisGeneral.lean, Quantum/SpinS/LiebSchultzMattisProof.lean, Quantum/SpinS/LiebSchultzMattisGlobalLocalReduction.lean, Quantum/SpinS/LiebSchultzMattisGeneratorNorm.lean, Quantum/SpinS/LiebSchultzMattisTaylorBound.lean, Quantum/SpinS/LiebSchultzMattisGeneralDischarge.lean, Math/MatrixAnalysis/HermitianExpUnitary.lean, Quantum/SpinS/ManyBodyOperatorNorm.lean |
IsHiddenAFMConfig / hhafProjection / tasaki_prop_6_5_hhaf_spin_one |
Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/HiddenAntiferromagneticOrder.lean + Quantum/SpinS/HiddenAntiferromagneticOrderUniqueness.lean + Quantum/SpinS/HiddenAntiferromagneticOrderUniquenessCore.lean |
The shared manyBodyOperatorNormS algebra and unitary-conjugation API is hosted by Quantum/SpinS/ManyBodyOperatorNorm.lean; the generic adjoint and two-sided unitarity identities for Hermitian-generated exponentials are hosted by Math/MatrixAnalysis/HermitianExpUnitary.lean.
← Bose–Einstein condensation of hard-core bosons (Tasaki §5.1–§5.2) · Catalogue · The AKLT model (Tasaki §7.1) →