Prove2Me

Eqs. (12), (33): Δb>Δ⇒(cos⁡r)Δb−Δ→0\Delta_b>\Delta\Rightarrow(\cos r)^{\Delta_b-\Delta}\to0

Proved
Giddings1999.multiparticle_boundary_suppression

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

ads-cftmathematical-physics

For real Δ<Δb\Delta<\Delta_b,

lim⁡r→π/2−(cos⁡r)Δb−Δ=0.\lim_{r\to\pi/2^-}(\cos r)^{\Delta_b-\Delta}=0 .

With the spectral assumption (12), Δb>Δ\Delta_b>\Delta for every multiparticle state, this is the vanishing of the limit (33). It gives eq. (30): the boundary operators afa_f do not connect the vacuum to multiparticle states.

Preamble
import Mathlib
import Definitions.Def_Giddings1999_AdSModes

open Real Filter Topology
Formal statement
namespace Giddings1999

/-- **Milestone, eqs. (12), (33)**: if `Δ_b > Δ` then `(cos r)^{Δ_b − Δ} → 0` as `r → π/2`. -/
theorem multiparticle_boundary_suppression (Δ Δb : ℝ) (h : Δ < Δb) :
    Tendsto (fun r => cos r ^ (Δb - Δ)) (𝓝[<] (π / 2)) (𝓝 0) := 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. (12), (30), (33), p. 2709
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