Prove2Me

Eq. (4): 2h±2h_\pm solve Δ(Δ−d)=m2R2\Delta(\Delta-d)=m^2R^2 and 2h+−2h−=2ν2h_+-2h_-=2\nu

Proved
Giddings1999.twoH_indicial_roots

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

ads-cftmathematical-physics

For every d∈Nd\in\mathbb N and m,R∈Rm,R\in\mathbb R, with ν=12d2+4m2R2\nu=\tfrac12\sqrt{d^2+4m^2R^2} and 2h±=d2±ν2h_\pm=\tfrac d2\pm\nu,

2h+(2h+−d)=m2R2,2h−(2h−−d)=m2R2,2h+−2h−=2ν.2h_+(2h_+-d)=m^2R^2,\qquad 2h_-(2h_--d)=m^2R^2,\qquad 2h_+-2h_-=2\nu .

These are the two boundary exponents of the radial equation at r=π/2r=\pi/2: (cos⁡r)2h+(\cos r)^{2h_+} is the decay of normalizable modes (eq. 6) and (cos⁡r)2h−(\cos r)^{2h_-} the growth of non-normalizable ones (eq. 9).

Preamble
import Mathlib
import Definitions.Def_Giddings1999_AdSModes

open Real Filter Topology
Formal statement
namespace Giddings1999

/-- **Milestone, eq. (4)**: `2h₊` and `2h₋` are the two roots of `Δ(Δ − d) = m²R²`, and they differ
by `2ν`. -/
theorem twoH_indicial_roots (d : ℕ) (m R : ℝ) :
    twoHPlus d m R * (twoHPlus d m R - d) = m ^ 2 * R ^ 2 ∧
    twoHMinus d m R * (twoHMinus d m R - d) = m ^ 2 * R ^ 2 ∧
    twoHPlus d m R - twoHMinus d m R = 2 * nu d m R := 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, eq. (4), 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