Prove2Me

Eqs. (8)–(9): off the spectrum, a regular solution with χωl∼(cos⁡r)2h−\chi_{\omega l}\sim(\cos r)^{2h_-} exists

Proved
Giddings1999.nonNormalizable_mode_exists

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

ads-cftmathematical-physics

Let d≥2d\ge2, R>0R>0, m∈Rm\in\mathbb R, l∈Nl\in\mathbb N, and let ω∈R\omega\in\mathbb R satisfy ∣ω∣≠ωnl|\omega|\neq\omega_{nl} for every n∈Nn\in\mathbb N. Then there is a solution χωl\chi_{\omega l} of the radial equation at frequency ω\omega that is bounded near r=0r=0 and satisfies

lim⁡r→π/2−χωl(r)(cos⁡r)2h−=1.\lim_{r\to\pi/2^-}\frac{\chi_{\omega l}(r)}{(\cos r)^{2h_-}}=1 .

These are the non-normalizable modes ϕωlm⃗=e−iωtYlm⃗χωl\phi_{\omega l\vec m}=e^{-i\omega t}Y_{l\vec m}\chi_{\omega l} of eq. (8), in the normalization convention of eq. (9).

Formalization Note The paper says these solutions exist "at arbitrary frequency". At ∣ω∣=ωnl|\omega|=\omega_{nl} the solution that is regular at r=0r=0 is the normalizable χnl\chi_{nl}, so the coefficient of (cos⁡r)2h−(\cos r)^{2h_-} cannot be normalized to 11. The statement therefore excludes the spectrum.

Preamble
import Mathlib
import Definitions.Def_Giddings1999_AdSModes

open Real Filter Topology
Formal statement
namespace Giddings1999

/-- **Milestone, eqs. (8), (9)**: away from the normalizable spectrum, there is a solution regular at
the origin with boundary behaviour `χ_{ωl}(r) → (cos r)^{2h₋}` (normalized coefficient `1`). -/
theorem nonNormalizable_mode_exists (d : ℕ) (hd : 2 ≤ d) (m R : ℝ) (hR : 0 < R) (ω : ℝ) (l : ℕ)
    (hω : ∀ n : ℕ, |ω| ≠ omegaNL d m R n l) :
    ∃ χ : ℝ → ℝ, IsRadialSolution d m R ω l χ ∧ IsRegularAtOrigin χ ∧
      Tendsto (fun r => χ r / cos r ^ twoHMinus d m R) (𝓝[<] (π / 2)) (𝓝 1) := by
  sorry

end Giddings1999
Source
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. (8), (9), p. 2707
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph