Generated formalization-status view. Do not edit this section by hand.
The interim legacy catalogue remains authoritative until Issue #5228.
Canonical record detail
The staggered order parameter of the one-dimensional antiferromagnetic Heisenberg ring vanishes in the thermodynamic-then-zero-field limit.
- Record ID
- tasaki-2020-theorem-4-2-shastry-no-ssb
- Lean declaration
- LatticeSystem.Quantum.shastry_no_symmetry_breaking_1d
- Declaration kind
- axiom
- Human status
- documented axiom
- Implementation state
- implemented
- Source coverage
- complete
- Trust state
- documented_axiom
- Capstone
- true
- Module
- LatticeSystem.Quantum.SpinS.ShastryNoSSB
- Source path
- LatticeSystem/Quantum/SpinS/ShastryNoSSB.lean
- Origin
- literature
- Topic
- quantum-spin
- Topic
- symmetry-breaking
- Axiom dependency
- LatticeSystem.Quantum.shastry_no_symmetry_breaking_1d
- Proof-guide anchor
- none
- Citation
- Physics and Mathematics of Quantum Many-Body Systems, theorem 4.2; section 4.1; equations 4.1.9, 4.1.10; pages 76-77 — Shastry absence of symmetry breaking in one dimension
- Citation
- Bounds for correlation functions of the Heisenberg antiferromagnet, article; pages L249-L253 — Static staggered-susceptibility bound argument
- Citation
- Absence of spontaneous symmetry breaking in the ground state of one-dimensional spin-orbital model, article; pages 908-909 — Absence of spontaneous symmetry breaking in the ground state of one-dimensional spin-orbital model