Prove2Me

Eqs. (5), (7): χnl\chi_{nl} solves the radial Klein–Gordon equation at ωnl\omega_{nl}

Proved
Giddings1999.modeRadial_isRadialSolution

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 and n,l∈Nn,l\in\mathbb N. The function χnl(r)=sin⁡lr (cos⁡r)2h+Pn(l+d/2−1,ν)(cos⁡2r)\chi_{nl}(r)=\sin^l r\,(\cos r)^{2h_+}P_n^{(l+d/2-1,\nu)}(\cos 2r) is C2C^2 on (0,π/2)(0,\pi/2) and satisfies there

χ′′+d−1sin⁡rcos⁡rχ′+ωnl2χ−l(l+d−2)sin⁡2rχ−m2R2cos⁡2rχ=0,ωnl=2h++2n+l.\chi''+\frac{d-1}{\sin r\cos r}\chi'+\omega_{nl}^2\chi-\frac{l(l+d-2)}{\sin^2 r}\chi-\frac{m^2R^2}{\cos^2 r}\chi=0,\qquad \omega_{nl}=2h_++2n+l .

Equivalently, e−iωnltYlm⃗χnle^{-i\omega_{nl}t}Y_{l\vec m}\chi_{nl} solves the free equation (□−m2)ϕ=0(\Box-m^2)\phi=0 (eq. 3) on global AdSd+1\mathrm{AdS}_{d+1}.

Preamble
import Mathlib
import Definitions.Def_Giddings1999_AdSModes

open Real Filter Topology
Formal statement
namespace Giddings1999

/-- **Milestone, eqs. (5), (7)**: `χ_{nl}` solves the radial free equation at frequency `ω_{nl}`. -/
theorem modeRadial_isRadialSolution (d : ℕ) (hd : 2 ≤ d) (m R : ℝ) (hR : 0 < R) (n l : ℕ) :
    IsRadialSolution d m R (omegaNL d m R n l) l (modeRadial d m R n l) := 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. (5), (7), p. 2707; explicit form from Balasubramanian–Kraus–Lawrence, hep-th/9805171 (the paper's ref. [10])
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