Three-state vacuum and ferromagnetic-row switch

Definition

usg_three_state_switch

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

mathematical-physicsquantum-informationspectral-gaptheoretical-computer-scienceundecidability

Each site has a vacuum level 0 and spin levels 1,2. Let P be the occupied-site projector, G the diagonal projector onto vacuum/occupied edge pairs, and F the rank-one operator generated by |1,2⟩−|2,1⟩. The model has on-site term aP, horizontal term G+bF, and vertical term G. Thus its all-occupied sector consists of independent ferromagnetic rows with the scalar shift aL². The auxiliary set records sums of one-magnon path-Laplacian energies, one per row:

S_L(b)=\left\{\sum_{r=1}^{L}2b(1-\cos(\pi k_r/L)):0\le k_r<L\right\}.

These are definitions only; spectral containment and density are separate proof obligations.

Definition code

import Definitions.Def_usg_spectral_notions

set_option autoImplicit false

namespace UndecidableSpectralGap

/-- Level 0 is vacuum; levels 1 and 2 carry a spin. -/
def switchProjector : Matrix (Fin 3) (Fin 3) ℂ :=
  fun i j => if i = j ∧ i ≠ 0 then 1 else 0

/-- Unit cost for an edge joining vacuum to an occupied site. -/
def switchGuard : Matrix (Fin 3 × Fin 3) (Fin 3 × Fin 3) ℂ :=
  fun i j => if i = j ∧ ((i.1 = 0 ∧ i.2 ≠ 0) ∨ (i.1 ≠ 0 ∧ i.2 = 0)) then 1 else 0

def switchVector (i : Fin 3 × Fin 3) : ℤ :=
  if i = (1, 2) then 1 else if i = (2, 1) then -1 else 0

/-- The positive exchange operator I-swap on the occupied two-spin block. -/
def switchExchange : Matrix (Fin 3 × Fin 3) (Fin 3 × Fin 3) ℂ :=
  fun i j => (switchVector i : ℂ) * (switchVector j : ℂ)

noncomputable def switchHam (L : ℕ) (a b : ℝ) :=
  latticeHam L 3 ((a : ℂ) • switchProjector)
    (switchGuard + (b : ℂ) • switchExchange) switchGuard

/-- At most one magnon in each independent occupied row. -/
def switchMagnonSpectrum (L : ℕ) (b : ℝ) : Set ℝ :=
  {s | ∃ k : Fin L → Fin L,
    s = ∑ r : Fin L, 2 * b * (1 - Real.cos (Real.pi * (k r : ℝ) / (L : ℝ)))}

end UndecidableSpectralGap

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