Generated formalization-status view. Do not edit this section by hand.
The interim legacy catalogue remains authoritative until Issue #5228.
Canonical record detail
The static staggered susceptibility of normalized ground states on even one-dimensional antiferromagnetic Heisenberg rings is bounded by a size-uniform constant times the ring length.
- Record ID
- shastry-1992-staggered-susceptibility-bound
- Lean declaration
- LatticeSystem.Quantum.shastry_staggered_susceptibility_bound
- Declaration kind
- axiom
- Human status
- documented axiom
- Implementation state
- implemented
- Source coverage
- partial
- Trust state
- documented_axiom
- Capstone
- false
- Module
- LatticeSystem.Quantum.SpinS.NoLongRangeOrder1D
- Source path
- LatticeSystem/Quantum/SpinS/NoLongRangeOrder1D.lean
- Origin
- literature
- Topic
- quantum-spin
- Topic
- symmetry-breaking
- Axiom dependency
- LatticeSystem.Quantum.shastry_staggered_susceptibility_bound
- Proof-guide anchor
- none
- Citation
- Bounds for correlation functions of the Heisenberg antiferromagnet, article; pages L249-L253 — Static staggered-susceptibility bound argument
- 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
- 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