Densitized mode Hamiltonian is essentially self-adjoint

Definition

ChapterQuantumGravityDensitizedProofs

by hitme development · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

spectral-theorytimepiece

In the Hermite basis the gravity fiber is multiplication by a real mode symbol. Faris–Lavine already proves every real multiplication operator on its maximal domain in ℓ² is essentially self-adjoint, so the densitized mode Hamiltonian inherits that conclusion with no extra bound.

H_k = \tfrac{1}{16}a_k^2 - \tfrac{1}{24}b_k^2 + V_k \qquad\Longrightarrow\qquad H\ \mathrm{esa\ on\ }D_{\max}(\ell^2).

Formalization Note. Lean name BookProof.QuantumGravityDensitized.qgModeHamiltonian_essentiallySelfAdjoint. Husk defs stay in ChapterQuantumGravityDensitized.

Definition code

import Mathlib
import Definitions.Def_ChapterQuantumGravityDensitized
import Definitions.Def_ChapterFarisLavine
import Theorems.Thm_BookProof_FarisLavine_mulHamiltonian_essentiallySelfAdjoint

namespace BookProof.QuantumGravityDensitized

open BookProof.FarisLavine

noncomputable section

theorem qgModeHamiltonian_essentiallySelfAdjoint (a b V : ℕ → ℝ) :
    EssentiallySelfAdjointOn (mulSymbolDomain (qgModeSymbol a b V))
      (qgModeHamiltonian a b V) :=
  mulHamiltonian_essentiallySelfAdjoint _

end

end BookProof.QuantumGravityDensitized

Source

timepiece BookProof, ChapterQuantumGravityDensitized.lean, theorem qgModeHamiltonian_essentiallySelfAdjoint

View graph