Avila-Jitomirskaya Ten Martini Problem

ten_martini_problem — a formalization challenge from the lean-eval benchmark.

Notes

The theorem constructs the almost Mathieu operator as an actual Mathlib continuous linear endomorphism of lp (fun _ : Int => Complex) 2; IsAlmostMathieuOperator fixes it by the standard coordinate formula, rather than hiding it in trusted spectral scaffolding. For irrational frequency alpha, nonzero coupling lambda, and arbitrary phase theta, its complex spectrum is asserted to be nonempty, compact, perfect, and totally disconnected, i.e. a Cantor set. Including operator existence in the conclusion prevents vacuity through an uninhabited formula predicate.

Formal statement

/-- **Avila-Jitomirskaya Ten Martini theorem.** For irrational frequency
and nonzero coupling, the spectrum of the almost Mathieu operator is a
Cantor set. Here this means nonempty, compact, perfect, and totally
disconnected. -/
theorem ten_martini_problem (α coupling θ : ℝ)
    (hα : Irrational α) (hcoupling : coupling ≠ 0) :
    ∃ H : EllTwo →L[ℂ] EllTwo,
      IsAlmostMathieuOperator α coupling θ H ∧
        (spectrum ℂ H).Nonempty ∧
        IsCompact (spectrum ℂ H) ∧
        Perfect (spectrum ℂ H) ∧
        IsTotallyDisconnected (spectrum ℂ H) := by
  sorry

Informal solution sketch

Aubry duality relates the almost Mathieu operators at couplings lambda and 1/lambda, so the proof can combine localization information in one regime with reducibility information in the dual regime. Avila and Jitomirskaya establish nonperturbative localization estimates and analyze the associated quasiperiodic SL(2,R) cocycles. For every irrational frequency and nonzero coupling, these estimates rule out intervals in the spectrum and also rule out isolated spectral points. Standard self-adjoint spectral theory supplies nonemptiness and compactness. Thus the spectrum is compact and perfect with no nontrivial connected subsets, which is precisely the Cantor-set conclusion stated in Lean.

Source

A. Avila and S. Jitomirskaya, 'The Ten Martini Problem', Ann. of Math. 170 (2009), 303-342, https://doi.org/10.4007/annals.2009.170.303.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: ten_martini_problem
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.