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 |
|---|---|---|
xyHamiltonianS / tasaki_5_1_xy_odlro_half_filling |
Theorem 5.1 (§5.1–§5.2, AXIOM; eqs. (5.1.1)–(5.2.5)): off-diagonal long-range order (ODLRO) of hard-core bosons at half filling. Hard-core bosons (u↑∞ limit of the bosonic Hubbard model, eq. 5.1.4) are equivalent to the S=1/2 XY model (eq. 5.1.5) via the identification â_x†↔(−1)^x Ŝ_x^+, n̂_x↔Ŝ_x^(3)+½, N̂↔Ŝ_tot^(3)+L^d/2 (eqs. 5.1.6–5.1.7); half filling ρ=½ ↔ the Ŝ_tot^(3)=0 sector. xyHamiltonianS d L = the XY Hamiltonian (XXZ at λ=D=0, N=1). The bosonic order operators Ô_L^(1,2) (eqs. 5.2.2/5.2.4) are the staggered XY-plane spin order operators. For d ≥ 2 (hd : 2 ≤ d) and half filling, ODLRO holds with q₀ > 0 (depending only on d): every ground state Φ_GS (eigenvector + min-energy, Φ≠0, Ŝ_tot^(3) Φ=0) of xyHamiltonianS satisfies ⟨(Ô_L^(α))²⟩/⟨Φ,Φ⟩/(L^d)² ≥ q₀ for α=1,2 (α:Fin 3, α≠2) and all large even L (eq. 5.2.5; the squared operator Ô_L^(α)/L^d gives the (L^d)² denominator, the intensive ODLRO density). Half filling is essential; the ground state shows LRO without SSB (eq. 5.2.8). Proof: reflection positivity (Kennedy–Lieb–Shastry, Kubo–Kishi). The recorded statement is uniform-in-L finite-dimensional (same pattern as the discharged Thm 4.6/4.8/4.9/4.11), not a true infinite-volume claim; it is a documented axiom because the d-dim reflection-positivity / infrared-bound proof technique is intractable at project scale (the existing RP infrastructure is 1D-ring-only), not because the subject is infinite-volume. Rectification: it returns to a prove-target if a d-dim RP/IR-bound infrastructure is ever built |
Quantum/SpinS/BoseEinsteinCondensate.lean |
xyChemicalPotentialHamiltonianS / IsBECTowerConstantsHalfFilling / tasaki_5_2_bec_tower_half_filling / tasaki_5_2_bec_tower |
Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/BoseEinsteinCondensate.lean, Quantum/SpinS/BoseEinsteinCondensateAlgebra.lean, Quantum/SpinS/BoseEinsteinCondensateMoment.lean, Quantum/SpinS/BoseEinsteinCondensateDenominator.lean, Quantum/SpinS/BoseEinsteinCondensateXYNumerator.lean, Quantum/SpinS/BoseEinsteinCondensateTower.lean |
becCoherentState / IsBECCoherentSSBConstants / tasaki_5_3_bec_u1_ssb / IsBECCoherentSSBConstantsHalfFilling / becCoherentState_dotProduct_mulVec / becCoherent_complexMoment_raising / becCoherent_complexMoment_lowering / becCoherent_secondMoment1_eq / becCoherent_secondMoment2_eq |
Long-form authoritative record. The complete statement and implementation chronicle are in the grouped detail record. | Quantum/SpinS/BoseEinsteinCondensate.lean, Quantum/SpinS/BoseEinsteinCondensateSector.lean, Quantum/SpinS/BoseEinsteinCondensateCoherentMatrixElement.lean, Quantum/SpinS/BoseEinsteinCondensateCoherentMoment.lean, Quantum/SpinS/BoseEinsteinCondensateCoherentConcentration.lean, Quantum/SpinS/BoseEinsteinCondensateCoherentSecondMoment.lean, Quantum/SpinS/BoseEinsteinCondensateCoherentSecondMomentConcentration.lean, Quantum/SpinS/BoseEinsteinCondensateCoherentAssembly.lean |
CoupledSite / coupledHamiltonian / coupledCrossCorrelation / tasaki_5_4_coupled_bec_ssb |
Theorem 5.4 (§5.5, AXIOM; eqs. (5.5.1)–(5.5.6)): symmetry breaking in coupled BEC. The coupled two-species lattice CoupledSite = HypercubicTorus × Bool ((x,false)=a, (x,true)=b); total Hamiltonian Ĥ_tot^ε = Ĥ_a + Ĥ_b + ε Ĥ_tunnel (coupledHamiltonian, eq. 5.5.1): the two uncoupled boson copies Ĥ_a+Ĥ_b = 2(Ĥ_XY,a+Ĥ_XY,b) (the boson factor Ĥ=2Ĥ_XY, consistent with xyChemicalPotentialHamiltonianS, so ε is the textbook tunneling strength; via sameSpeciesNNCoupling) + the tunneling term tunnelHamiltonian φ = −Σ_x (e^{iφ} Ŝ^+_a Ŝ^−_b + e^{−iφ} Ŝ^−_a Ŝ^+_b) (eq. 5.5.3). Total 2N particles = doubled half filling Ŝ_tot^(3)=0. Assuming single-system ODLRO (hODLRO: the uncoupled XY ground states satisfy the Theorem 5.1 bound with q₀, tying q₀ to genuine ODLRO), the unique coupled ground state Φ^ε develops a definite relative U(1) phase: ∃ m̃ ≥ √(2q₀) with lim_{ε↓0} lim_{L↑∞} ⟨Φ^ε, â†_{(x,a)}â_{(x,b)} Φ^ε⟩/⟨Φ^ε,Φ^ε⟩ = m̃²e^{−iφ} (eq. 5.5.5; coupledCrossCorrelation = Ŝ^+_{(x,a)}Ŝ^−_{(x,b)}) and the conjugate ⟨Φ^ε, â_{(x,a)}â†_{(x,b)} Φ^ε⟩/⟨·⟩ = m̃²e^{+iφ} (eq. 5.5.6; coupledCrossCorrelationConj = Ŝ^−_{(x,a)}Ŝ^+_{(x,b)}). Double limit in eventual-ε' form (outer ε↓0, inner L↑∞); GS family given (unique by MLM). The two condensates are coherently coupled (entangled). Proof: Koma–Tasaki [22]. Documented axiom because this is a genuine iterated thermodynamic limit lim_{ε↓0} lim_{L↑∞}: a Tasaki footnote states that the existence of the limit itself is unproven (open in the source literature), so it falls under the open-conjecture exclusion of the externally-cited-theorem prove policy. Completes Tasaki Chapter 5 |
Quantum/SpinS/BoseEinsteinCondensate.lean |
← Horsch–von der Linden low-lying states (Tasaki §3.4, Theorem 3.1) · Catalogue · Antiferromagnetic Heisenberg chains and the Haldane conjecture (Tasaki §6.1) →