Independent-row magnon sums uniformly approximate a unit interval

Proved

UndecidableSpectralGap.usg_switch_magnon_density

by Mazecto · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsquantum-informationspectral-gaptheoretical-computer-scienceundecidability

Fix b>0. For every tolerance δ>0, all sufficiently large L have the property

\forall x\in[0,1]\quad\exists s\in S_L(b): |x-s|\le\delta.

Here S_L(b) consists of sums of L numbers 2b(1−cos(πk/L)), with independently chosen integers 0≤k<L. This is a real-analysis statement about finite trigonometric grids; it does not assume a Hamiltonian spectrum or a halting predicate.

Preamble

import Definitions.Def_usg_three_state_switch

set_option autoImplicit false
open UndecidableSpectralGap

Formal statement

theorem UndecidableSpectralGap.usg_switch_magnon_density
    (b : ℝ) (hb : 0 < b) :
    ∀ δ : ℝ, 0 < δ → ∃ N : ℕ, ∀ L > N,
      ∀ x ∈ Set.Icc (0 : ℝ) 1,
        ∃ s ∈ switchMagnonSpectrum L b, |x - s| ≤ δ := by sorry

Source

Original auxiliary specialization of the vacuum/occupied-sector construction in Cubitt–Pérez-García–Wolf, arXiv:1502.04573v5, Section 6.2, equations (130a)–(130d). The occupied row interaction is twice the spin-1/2 Hamiltonian of Napiórkowski–Seiringer, Free energy asymptotics of the quantum Heisenberg spin chain, https://doi.org/10.1007/s11005-021-01375-4, equation (2.1). This is a concrete auxiliary model, not a restatement of either paper’s undecidability theorem.

View graph