quantum_unique_ergodicity

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Proved status carries no information about that problem. Do not import this node or use it as a dependency.

Quantum unique ergodicity (QUE) conjecture (Rudnick–Sarnak 1994): For compact hyperbolic surfaces, the eigenfunctions of the Laplacian equidistribute as the eigenvalue → ∞. Proved for arithmetic surfaces (Lindenstrauss 2006, Fields Medal). Open for general compact hyperbolic surfaces.

Why this node was retired

The posted statement is

import Mathlib

theorem quantum_unique_ergodicity (n : ℕ) (hn : 1 ≤ n)
    (T : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))
    (hT : T.IsSymmetric)
    (psi_n : ℕ → EuclideanSpace ℝ (Fin n))
    (hlambda : ∀ k, T (psi_n k) = (k : ℝ) • psi_n k)
    (hnorm : ∀ k, ‖psi_n k‖ = 1) :
    Filter.Tendsto (fun k =>
      fun A : Set (EuclideanSpace ℝ (Fin n)) =>
        (MeasureTheory.volume A).toReal * ‖psi_n k‖^2)
    Filter.atTop (nhds (fun A => (MeasureTheory.volume A).toReal)) := by
  sorry

The purported distribution is volume(A) times the global norm squared, already volume(A) by normalization; no eigenfunction mass is integrated. Infinitely many normalized eigenvectors with eigenvalues k in a fixed finite-dimensional space are also impossible.

A proof of a malformed proposition can be a correct proof of that proposition, so this is not a judgment on the accepted submission — but the Proved status must not be read as settling the problem shown above.

Proposed corrected statement

On a specified compact hyperbolic surface M, take L²-normalized Laplace eigenfunctions ψⱼ with eigenvalues tending to infinity and assert weak convergence of |ψⱼ|²dvol to dvol/vol(M): for every continuous test function f, ∫f|ψⱼ|²→vol(M)⁻¹∫f. Specify any Hecke/arithmetic restrictions if a proved variant is intended.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.