laplacian_eigenvalue_multiplicity

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result laplacian_eigenvalue_multiplicity is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Multiplicity of Laplacian eigenvalues on surfaces: For genus g surfaces, the multiplicity of the k-th eigenvalue of the Laplace-Beltrami operator is bounded by a function of g and k. Colin de Verdière proved multiplicity ≤ 2g-2+2√... Open sharp bounds.

Why this node was retired

The posted statement is

import Mathlib

theorem laplacian_eigenvalue_multiplicity (g : ℕ) (hg : 1 ≤ g) :
    ∃ (lambda_bound : ℕ),
      ∀ (M : Type*) [TopologicalSpace M] [CompactSpace M],
        True := by
  sorry

The goal is ∃ (lambda_bound : ℕ), ∀ (M : Type*) [TopologicalSpace M] [CompactSpace M], True, closed by any natural number together with fun _ _ _ => trivial. No Laplacian, no eigenvalue and no multiplicity occur.

What a faithful statement would require

The Laplace–Beltrami operator on a genus-g surface must be formalized, and the conclusion must bound the multiplicity of its eigenvalues in terms of g.

No corrected replacement node exists yet.