Model for Shomer's black-hole vs CFT entropy argument

Definition

GravityNonRenorm_Defs

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

black-holesconformal-field-theoryquantum-gravity

This definition file fixes the physical model used by every statement of the mission (Shomer, arXiv:0709.3555, Secs. IV–V).

$\mathrm{Vol}(S^n)=\dfrac{2\pi^{(n+1)/2}}{\Gamma\!\left(\frac{n+1}{2}\right)}$ , the area of the unit round sphere $S^n$ (sphereArea n).
$\omega_n=\dfrac{16\pi}{n\,\mathrm{Vol}(S^n)}$ , the constant appearing below Eq. (31) (omega n).
The CFT entropy as a function of energy (Eqs. 29–30): with $T(E)=\bigl(E/(bR^{d-1})\bigr)^{1/d}$ ,

S_{\rm CFT}(E)=a\,\bigl(R\,T(E)\bigr)^{d-1}

(cftEntropyOfEnergy d a b R E). 4. The Schwarzschild and Schwarzschild–AdS metric functions (Eqs. 31, 33):

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

The Bekenstein–Hawking entropy $S=A/(4G_N)$ .
The horizon radius $r_H$ = the supremum (largest element) of the set of positive zeros of $f$ (resp. $f_{\rm AdS}$ ), and the black-hole entropy $S_{\rm BH}(M)=\mathrm{Vol}(S^{d-2})\,r_H^{d-2}/(4G_N)$ (Eqs. 32, 34).

These definitions are the shared model on which every theorem of the mission is stated.

Formalization Note Horizon radii use sSup, which returns $0$ on an empty (or unbounded) set; the mission's statements only use them for $M>0$ or asymptotically. Natural-number subtraction is used in exponents such as $d-3$ ; statements carry the dimension bounds that make these exact.

Definition code

import Mathlib

namespace GravityNonRenorm

open Real

/-- Area (`(n)`-dimensional volume) of the unit round sphere `Sⁿ ⊂ ℝⁿ⁺¹`:
`Vol(Sⁿ) = 2 π^{(n+1)/2} / Γ((n+1)/2)`. -/
noncomputable def sphereArea (n : ℕ) : ℝ :=
  2 * π ^ (((n : ℝ) + 1) / 2) / Real.Gamma (((n : ℝ) + 1) / 2)

/-- Shomer's constant `ω_n = 16π / (n · Vol(Sⁿ))` (text below Eq. (31)). -/
noncomputable def omega (n : ℕ) : ℝ :=
  16 * π / ((n : ℝ) * sphereArea n)

/-- Entropy of a `d`-dimensional conformal field theory on `ℝ_time × S^{d-1}` (sphere radius `R`)
as a function of its energy `E`, obtained from Eq. (29), `S = a (RT)^{d-1}`, `E = b R^{d-1} T^d`,
by eliminating the temperature: `T(E) = (E / (b R^{d-1}))^{1/d}` and `S(E) = a (R T(E))^{d-1}`. -/
noncomputable def cftEntropyOfEnergy (d : ℕ) (a b R E : ℝ) : ℝ :=
  a * (R * (E / (b * R ^ (d - 1))) ^ ((1 : ℝ) / d)) ^ (d - 1)

/-- Metric function of the `d`-dimensional Schwarzschild solution, Eq. (31):
`f(r) = 1 - ω_{d-2} G_N M / r^{d-3}`. -/
noncomputable def schwarzschildF (d : ℕ) (G M r : ℝ) : ℝ :=
  1 - omega (d - 2) * G * M / r ^ (d - 3)

/-- Metric function of the `d`-dimensional Schwarzschild–AdS solution, Eq. (33):
`f(r) = 1 - ω_{d-2} G_N M / r^{d-3} + r² / R_AdS²`. -/
noncomputable def adsSchwarzschildF (d : ℕ) (G M RAdS r : ℝ) : ℝ :=
  1 - omega (d - 2) * G * M / r ^ (d - 3) + r ^ 2 / RAdS ^ 2

/-- Bekenstein–Hawking entropy `S = A / (4 G_N)` of a horizon of area `A`. -/
noncomputable def bekensteinHawkingEntropy (G A : ℝ) : ℝ :=
  A / (4 * G)

/-- Horizon radius of the `d`-dimensional Schwarzschild black hole of mass `M`:
the largest positive zero of `f` (Eq. (31)). -/
noncomputable def flatHorizonRadius (d : ℕ) (G M : ℝ) : ℝ :=
  sSup {r : ℝ | 0 < r ∧ schwarzschildF d G M r = 0}

/-- Horizon radius of the `d`-dimensional Schwarzschild–AdS black hole of mass `M`:
the largest positive zero of `f` (Eq. (33)). -/
noncomputable def adsHorizonRadius (d : ℕ) (G M RAdS : ℝ) : ℝ :=
  sSup {r : ℝ | 0 < r ∧ adsSchwarzschildF d G M RAdS r = 0}

/-- Bekenstein–Hawking entropy of the `d`-dimensional Schwarzschild black hole of energy `M`,
Eq. (32): horizon area `A = Vol(S^{d-2}) r_H^{d-2}`. -/
noncomputable def flatBHEntropy (d : ℕ) (G M : ℝ) : ℝ :=
  bekensteinHawkingEntropy G (sphereArea (d - 2) * flatHorizonRadius d G M ^ (d - 2))

/-- Bekenstein–Hawking entropy of the `d`-dimensional Schwarzschild–AdS black hole of energy `M`,
Eq. (34): horizon area `A = Vol(S^{d-2}) r_H^{d-2}`. -/
noncomputable def adsBHEntropy (d : ℕ) (G M RAdS : ℝ) : ℝ :=
  bekensteinHawkingEntropy G (sphereArea (d - 2) * adsHorizonRadius d G M RAdS ^ (d - 2))

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, Sec. IV Eqs. (29)-(30), Sec. V Eqs. (31)-(34)

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.

The file declares, in namespace GravityNonRenorm, the following real-valued functions. Conventions: $\pi$ is the real number pi and $\Gamma$ the real Gamma function; every power with a real exponent is a real power (for a negative base it follows Mathlib's convention, and it equals $1$ when the exponent is $0$ ); every subtraction between natural numbers ( $d-1$ , $d-2$ , $d-3$ ) is truncated at $0$ ; division by zero returns $0$ .

For $n\in\mathbb N$ : $\mathrm{sphereArea}(n)=2\pi^{(n+1)/2}/\Gamma((n+1)/2)$ .
For $n\in\mathbb N$ : $\omega_n=16\pi/(n\cdot \mathrm{sphereArea}(n))$ . For $n=0$ the denominator is $0$ , so $\omega_0=0$ .
For $d\in\mathbb N$ and reals $a,b,R,E$ :

\mathrm{cftEntropyOfEnergy}(d,a,b,R,E)=a\cdot\Bigl(R\cdot\bigl(E/(b\,R^{d-1})\bigr)^{1/d}\Bigr)^{d-1},

where $1/d$ is the real number $1/d$ (equal to $0$ when $d=0$ ) and the inner power is a real power. No sign conditions on $a,b,R,E$ are built in.

$\mathrm{schwarzschildF}(d,G,M,r)=1-\omega_{d-2}\,G\,M/r^{d-3}$ (natural-number power of $r$ ; if $r^{d-3}=0$ the fraction is $0$ ).
$\mathrm{adsSchwarzschildF}(d,G,M,R_{\rm AdS},r)=1-\omega_{d-2}\,G\,M/r^{d-3}+r^2/R_{\rm AdS}^2$ .
$\mathrm{bekensteinHawkingEntropy}(G,A)=A/(4G)$ .
$\mathrm{flatHorizonRadius}(d,G,M)=\sup\{r\in\mathbb R: r>0,\ \mathrm{schwarzschildF}(d,G,M,r)=0\}$ , where $\sup$ is the real supremum, which by convention is $0$ if the set is empty or not bounded above.
$\mathrm{adsHorizonRadius}(d,G,M,R_{\rm AdS})=\sup\{r>0:\mathrm{adsSchwarzschildF}(d,G,M,R_{\rm AdS},r)=0\}$ , same convention.
$\mathrm{flatBHEntropy}(d,G,M)=\mathrm{bekensteinHawkingEntropy}\bigl(G,\ \mathrm{sphereArea}(d-2)\cdot\mathrm{flatHorizonRadius}(d,G,M)^{d-2}\bigr)$ .
$\mathrm{adsBHEntropy}(d,G,M,R_{\rm AdS})=\mathrm{bekensteinHawkingEntropy}\bigl(G,\ \mathrm{sphereArea}(d-2)\cdot\mathrm{adsHorizonRadius}(d,G,M,R_{\rm AdS})^{d-2}\bigr)$ .

No theorems or hypotheses are stated in this file; it contains only these definitions.

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