Three-state switch local interaction-strength bound

Open

UndecidableSpectralGap.usg_switch_local_strength

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

mathematical-physicsquantum-informationspectral-gap

For parameters $0<b\le 1/2$ and $|a|\le b$ , the on-site projector, guarded horizontal exchange, and vertical guard of the three-state switch have combined local interaction strength at most one. In symbols,

\|aP\|+2\|G+bF\|+2\|G\|\le 1,

where the displayed expression denotes the model's normalized localInteractionStrength. This isolates the finite matrix-norm estimate from the many-body spectral analysis.

Preamble

import Definitions.Def_usg_three_state_switch

set_option autoImplicit false
open UndecidableSpectralGap

Formal statement

theorem UndecidableSpectralGap.usg_switch_local_strength
    (b a : ℝ) (hb : 0 < b) (hbhalf : b ≤ 1 / 2) (ha : |a| ≤ b) :
    localInteractionStrength ((a : ℂ) • switchProjector)
      (switchGuard + (b : ℂ) • switchExchange) switchGuard ≤ 1 := 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 precise normalization and matrices are those of Definitions.Def_usg_three_state_switch.

View graph