AdS black-hole entropy matches a $(d-1)$ -dimensional CFT

Proved

GravityNonRenorm.ads_entropy_matches_cft_one_dim_lower

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

black-holesquantum-gravity

Let $d\ge3$ , $G_N>0$ , $R_{\rm AdS}>0$ and $a,b,R>0$ . Let $S_{\rm AdS}(M)$ be the Bekenstein–Hawking entropy of the $d$ -dimensional Schwarzschild–AdS black hole of mass $M$ (Eq. 34), and let $S^{(d-1)}_{\rm CFT}(E)$ be the entropy-energy function (Eqs. 29–30) of a CFT in $d-1$ spacetime dimensions with data $a,b,R$ . Then, as $E\to\infty$ ,

S_{\rm AdS}(E)=\Theta\bigl(S^{(d-1)}_{\rm CFT}(E)\bigr).

Both grow like $E^{(d-2)/(d-1)}$ : AdS gravity in $d$ dimensions has the density of states of a CFT in one dimension fewer, as predicted by AdS/CFT.

Preamble

import Definitions.Def_GravityNonRenorm_Defs
import Mathlib

open GravityNonRenorm Filter Asymptotics

Formal statement

namespace GravityNonRenorm
theorem ads_entropy_matches_cft_one_dim_lower (d : ℕ) (hd : 3 ≤ d) (G RAdS a b R : ℝ)
    (hG : 0 < G) (hRAdS : 0 < RAdS) (ha : 0 < a) (hb : 0 < b) (hR : 0 < R) :
    (fun M : ℝ => adsBHEntropy d G M RAdS) =Θ[atTop]
      (fun E : ℝ => cftEntropyOfEnergy (d - 1) a b R E) := by sorry
end GravityNonRenorm

Source

Assaf Shomer, A pedagogical explanation for the non-renormalizability of gravity, arXiv:0709.3555v2 [hep-th] (2007), https://arxiv.org/abs/0709.3555

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement (at the explicit request of the proposal owner), not by a blind, independent auditor. The author knew the intended meaning and the source paper while writing it, so it must not be mistaken for independent testimony; reviewers should compare it against the Lean code themselves.

For every natural number $d\ge3$ and all strictly positive reals $G,R_{\rm AdS},a,b,R$ , the function $M\mapsto\mathrm{adsBHEntropy}(d,G,M,R_{\rm AdS})$ is $\Theta$ of $E\mapsto\mathrm{cftEntropyOfEnergy}(d-1,a,b,R,E)$ as the common real argument tends to $+\infty$ ; here $d-1$ is natural-number subtraction (exact, $\ge2$ ). Here $f=\Theta(g)$ as $x\to\infty$ (Mathlib's IsTheta along atTop) means: there are constants $c_1,c_2>0$ and $x_0$ such that $|f(x)|\le c_1|g(x)|$ and $|g(x)|\le c_2|f(x)|$ for all $x\ge x_0$ .

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

AdS black-hole entropy matches a (d−1)(d-1)(d−1)-dimensional CFT

AdS black-hole entropy matches a $(d-1)$ -dimensional CFT