Papers With

← All papers
First page of Persistence of Unitary Almost Mathieu Operator Gaps Ten Dry Martinis, Five on the Rim

Persistence of Unitary Almost Mathieu Operator Gaps Ten Dry Martinis, Five on the Rim

Dan S. Borgnia, Matthew Faust, Long Li

math-ph Oct 30, 2026 · v1 cond-mat.mes-hall math.SP quant-ph
formalization mathlib analysis physics
Read PDF arXiv abstract
TL;DR
The main gap-labeling theorem is stated in Lean using Mathlib definitions and formally verified, with a Lean statement and verification index in Appendix C.
Abstract
We determine exactly which gap labels are realized by open spectral gaps for the unitary almost Mathieu operator at every irrational frequency and all coupling constants ($0<λ_1,λ_2\leq1$). When both couplings are strictly less than one, every permitted gap label is realized by an open gap, including in the critical case ($λ_1=λ_2$). When at least one coupling equals one, both lifts of every odd winding label are realized by open gaps, whereas all even winding labels are collapsed. The proof combines quantitative almost reducibility and Aubry duality with a monotonicity principle for gap heights.
Problem

The paper determines exactly which gap labels permitted by the Gap Labeling Theorem are realized by open spectral gaps of the unitary almost Mathieu operator. It covers all irrational frequencies and all couplings 0<λ1,λ2≤1, a Dry Ten Martini-type question for this model.

Approach

The noncritical case is handled with quantitative almost reducibility and Aubry duality, using a positive-twist property of the Szegő cocycle. Boundary couplings are treated by a symmetry argument for even winding numbers and a perturbative argument for odd seed gaps. A height-function monotonicity principle, adapted from work on the critical almost Mathieu operator via a magnetic rotation algebra, continues gaps to the critical and boundary cases. The proof was formalized in Lean with Mathlib-based definitions, with help from AI tools.

Results

When both couplings are below one, every permitted gap label is realized by an open gap, including the critical case λ1=λ2. When at least one coupling equals one, both lifts of every odd winding label give open gaps and all even winding labels collapse. The final theorem statement is given in Lean together with a verification index.