Generated formalization-status view. Do not edit this section by hand.
The interim legacy catalogue remains authoritative until Issue #5228.
Canonical record detail
A normalized low-Rayleigh-energy trial state orthogonal to a ground eigenvector yields a low-lying energy eigenstate; the long-range-order estimate remains an application input.
- Record ID
- tasaki-2020-theorem-3-1-finite-dimensional-core
- Lean declaration
- LatticeSystem.Quantum.horsch_vonderLinden_lowLying
- Declaration kind
- theorem
- Human status
- proved
- Implementation state
- implemented
- Source coverage
- conditional_reduction
- Trust state
- axiom_free
- Capstone
- true
- Module
- LatticeSystem.Quantum.HorschVonderLinden
- Source path
- LatticeSystem/Quantum/HorschVonderLinden.lean
- Origin
- literature
- Topic
- low-energy-spectrum
- Topic
- symmetry-breaking
- Axiom dependency
- none
- Proof-guide anchor
- none
- Citation
- Physics and Mathematics of Quantum Many-Body Systems, theorem 3.1; section 3.4; equations 3.4.7-3.4.12; pages 66-67 — Horsch-von der Linden low-lying state theorem