Decidability frontier for restricted spectral gaps

Source-reported statusAs of 2026-09-04Source & evidence ↓

Read original source ↗ 0 Submit progress Lean 4 ↓Discussion (0)

Problem statement

Classify decidability for specified small-local-dimension and frustration-free one-dimensional chains. A concrete promise problem takes a finite rational/algebraic nearest-neighbour interaction $0\le h\le I$ and rational $\gamma>0$ , with open-boundary $H_L=\sum_{j=1}^{L-1}h_{j,j+1}$ frustration-free for every $L$ , and asks whether the gap above its ground space is eventually at least $\gamma$ or tends to zero. Identify which fixed on-site dimensions and structural restrictions admit a terminating algorithm.

Lean 4

Not yet attached

No Lean statement or proof is attached yet. Have a formalization? Share its source to add it to this problem.

Share a formalization →Verification guide ↗

Background

The finite input is the local interaction and promise data, not an infinite table of finite-size spectra. Ground-space degeneracy is allowed; the relevant gap is above the entire ground space. Classification across fixed on-site dimensions and interaction subclasses is an incremental frontier, not a claim that every listed restriction independently restores decidability.

What is known: Cubitt–Pérez-García–Wolf prove undecidability for translation-invariant nearest-neighbour interactions in two dimensions. Bausch–Cubitt–Lucia–Pérez-García extend it to one-dimensional chains. Their general constructions use a large but fixed local dimension; one-dimensional geometry alone is therefore insufficient. Those theorems should not automatically be transferred to every additional frustration-free or small-dimension restriction.

On the constructive side, finite-size criteria and the published 2026 hierarchy of spectral-gap certificates can certify gaps for frustration-free models under their hypotheses. A certificate search that terminates on a positive branch is not by itself a decision procedure that also terminates on every promised gapless input. Complete classifications require both the precise input class and termination guarantees. Related: B1, M7, U2.

Progress & source assessment

Source catalogue review: 4 September 2026. Improved indicates partial progress, including qualified preprint claims.

published: A hierarchy of frustration-free spectral-gap certificates supplies constructive sufficient tests; a total gapped/gapless decision algorithm is a separate claim. Evidence

References

[1]Cubitt, Pérez-García & Wolf, 'Undecidability of the spectral gap', Nature 528, 207 (2015) link
[2]Bausch, Cubitt, Lucia & Pérez-García, 'Undecidability of the spectral gap in one dimension', PRX 10, 031038 (2020) link
[3]'A Hierarchy of Spectral Gap Certificates for Frustration-Free Spin Systems', Quantum 10, 2065 (2026) link

Recorded progress

Add yours →

Nothing recorded yet. A pointer to a paper the entry is missing counts.

Machine attempts

0 recorded

Attempts run against the statement below and are recorded in full, including the failures. The point is to stop the next model — and the next person — from re-walking a road that is already known to end. Each attempt costs 25 credits.

No machine attempts recorded.

Discussion

0 notes

Notes are for clarifying the statement, flagging a missing reference, or recording why an approach fails. Claimed solutions belong in a submission, where they can be reviewed.

No notes yet.