Eqs. (3)–(7): normalizable modes of global occur exactly at
ProvedGiddings1999.normalizable_modes_classificationads-cftmathematical-physics
Let , , , and , and let , . A radial profile is a normalizable mode of the free Klein–Gordon equation on global with angular momentum and frequency (a nonzero solution of the radial equation that is regular at and has finite Klein–Gordon norm) if and only if there is with
and a constant such that on , where .
This is the statement of eqs. (5)–(7) that free solutions exist at every frequency but are normalizable only on the discrete spectrum , and that the normalizable ones are the modes .
Formalization Note "Regular at the origin" means is bounded on . "Finite Klein–Gordon norm" means is integrable on . The hypothesis gives , so the branch is never normalizable.
Preamble
import Mathlib import Definitions.Def_Giddings1999_AdSModes open Real Filter Topology
Formal statement
namespace Giddings1999
/-- **Goal** (eqs. 3–7): a radial profile `χ` is a normalizable mode of angular momentum `l` and
frequency `ω` iff `|ω| = ω_{nl} = 2h₊ + 2n + l` for some `n ∈ ℕ` and `χ` is a nonzero multiple of the
explicit mode `χ_{nl}` of eq. (5). -/
theorem normalizable_modes_classification (d : ℕ) (hd : 2 ≤ d) (m R : ℝ) (hR : 0 < R)
(ω : ℝ) (l : ℕ) (χ : ℝ → ℝ) :
IsNormalizableMode d m R ω l χ ↔
∃ n : ℕ, |ω| = omegaNL d m R n l ∧
∃ c : ℝ, c ≠ 0 ∧ Set.EqOn χ (fun r => c * modeRadial d m R n l r) (Set.Ioo 0 (π / 2)) := by
sorry
end Giddings1999Source
S. B. Giddings, Boundary S matrix and the anti-de Sitter space to conformal field theory dictionary, Phys. Rev. Lett. 83, 2707 (1999), https://doi.org/10.1103/PhysRevLett.83.2707, eqs. (3)–(7), p. 2707
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.