AdS black-hole entropy is not that of a $d$ -dimensional CFT

Proved

GravityNonRenorm.ads_entropy_not_cft

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 let $a,b,R>0$ be the data of a $d$ -dimensional CFT on $\mathbb R\times S^{d-1}$ as in Eq. (29). Let $S_{\rm AdS}(M)$ be the Bekenstein–Hawking entropy of the $d$ -dimensional Schwarzschild–AdS black hole of mass $M$ (Eq. 34) and $S_{\rm CFT}(E)$ the CFT entropy as a function of energy (Eq. 30). Then it is not the case that

S_{\rm AdS}(E)=\Theta\bigl(S_{\rm CFT}(E)\bigr)\qquad(E\to\infty).

So the high-energy density of states of $d$ -dimensional AdS gravity is not that of any $d$ -dimensional CFT of the form (29).

Preamble

import Definitions.Def_GravityNonRenorm_Defs
import Mathlib

open GravityNonRenorm Filter Asymptotics

Formal statement

namespace GravityNonRenorm
theorem ads_entropy_not_cft (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 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 reals $G,R_{\rm AdS},a,b,R$ , all strictly positive, it is false that the function $M\mapsto\mathrm{adsBHEntropy}(d,G,M,R_{\rm AdS})$ is $\Theta$ of the function $E\mapsto\mathrm{cftEntropyOfEnergy}(d,a,b,R,E)$ as the (common real) argument tends to $+\infty$ . Both functions are evaluated at the same real number; the CFT function uses the same $d$ as the black hole. 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 is not that of a ddd-dimensional CFT

AdS black-hole entropy is not that of a $d$ -dimensional CFT