Eq. (34): AdS black-hole entropy grows like $M^{(d-2)/(d-1)}$

Proved

GravityNonRenorm.ads_bh_entropy_eq34

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

black-holesquantum-gravity

Let $d\ge3$ , $G_N>0$ and $R_{\rm AdS}>0$ . For each mass $M$ let $r_H(M)$ be the largest positive zero of the Schwarzschild–AdS metric function

f(r)=1-\frac{\omega_{d-2}G_NM}{r^{d-3}}+\frac{r^2}{R_{\rm AdS}^2},

and let $S_{\rm AdS}(M)=\mathrm{Vol}(S^{d-2})\,r_H(M)^{d-2}/(4G_N)$ . Then, as $M\to\infty$ ,

S_{\rm AdS}(M)=\Theta\!\left(M^{\frac{d-2}{d-1}}\right).

This is Eq. (34): large AdS black holes have entropy growing like $M^{(d-2)/(d-1)}$ .

Preamble

import Definitions.Def_GravityNonRenorm_Defs
import Mathlib

open GravityNonRenorm Filter Asymptotics

Formal statement

namespace GravityNonRenorm
theorem ads_bh_entropy_eq34 (d : ℕ) (hd : 3 ≤ d) (G RAdS : ℝ) (hG : 0 < G) (hRAdS : 0 < RAdS) :
    (fun M : ℝ => adsBHEntropy d G M RAdS) =Θ[atTop]
      (fun M : ℝ => M ^ (((d : ℝ) - 2) / ((d : ℝ) - 1))) := 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>0$ , $R_{\rm AdS}>0$ , the function $M\mapsto\mathrm{adsBHEntropy}(d,G,M,R_{\rm AdS})$ is $\Theta$ of $M\mapsto M^{(d-2)/(d-1)}$ as $M\to+\infty$ (exponent computed in the reals, real power). Unfolded, $\mathrm{adsBHEntropy}(d,G,M,R_{\rm AdS})=\mathrm{sphereArea}(d-2)\,r_H^{d-2}/(4G)$ where $r_H$ is the real supremum of $\{r>0:\ 1-\omega_{d-2}GM/r^{d-3}+r^2/R_{\rm AdS}^2=0\}$ (value $0$ if that set is empty or unbounded). For $d=3$ the power $r^{d-3}$ is $r^0=1$ , so the defining equation becomes $1-\omega_1GM+r^2/R_{\rm AdS}^2=0$ . 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

Eq. (34): AdS black-hole entropy grows like M(d−2)/(d−1)M^{(d-2)/(d-1)}M(d−2)/(d−1)

Eq. (34): AdS black-hole entropy grows like $M^{(d-2)/(d-1)}$