Eq. (32): Schwarzschild black-hole entropy $S\propto M^{(d-2)/(d-3)}$

Proved

GravityNonRenorm.flat_bh_entropy_eq32

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

black-holesquantum-gravity

Let $d\ge4$ , $G_N>0$ and $M>0$ . Let $r_H$ be the largest positive zero of the Schwarzschild metric function $f(r)=1-\omega_{d-2}G_NM/r^{d-3}$ , where $\omega_n=16\pi/(n\,\mathrm{Vol}(S^n))$ , and let $S_{\rm BH}(M)=\mathrm{Vol}(S^{d-2})\,r_H^{d-2}/(4G_N)$ be the Bekenstein–Hawking entropy. Then

S_{\rm BH}(M)=\frac{\mathrm{Vol}(S^{d-2})}{4G_N}\,\bigl(\omega_{d-2}\,G_N\,M\bigr)^{\frac{d-2}{d-3}}.

This is the exact form of Eq. (32): the entropy of a flat-space black hole grows like $M^{(d-2)/(d-3)}$ .

Preamble

import Definitions.Def_GravityNonRenorm_Defs
import Mathlib

open GravityNonRenorm Filter Asymptotics

Formal statement

namespace GravityNonRenorm
theorem flat_bh_entropy_eq32 (d : ℕ) (hd : 4 ≤ d) (G M : ℝ) (hG : 0 < G) (hM : 0 < M) :
    flatBHEntropy d G M =
      sphereArea (d - 2) / (4 * G) *
        (omega (d - 2) * G * M) ^ (((d : ℝ) - 2) / ((d : ℝ) - 3)) := 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\ge4$ and all reals $G>0$ , $M>0$ :

\mathrm{flatBHEntropy}(d,G,M)=\frac{\mathrm{sphereArea}(d-2)}{4G}\cdot\bigl(\omega_{d-2}\,G\,M\bigr)^{\frac{d-2}{d-3}},

where $d-2$ inside $\mathrm{sphereArea}$ and $\omega$ is natural-number subtraction (exact here), the exponent $(d-2)/(d-3)$ is computed in the reals, and the power is a real power. Unfolding the definitions, the left side is $\mathrm{sphereArea}(d-2)\cdot r_H^{d-2}/(4G)$ with $r_H$ the real supremum of $\{r>0: 1-\omega_{d-2}GM/r^{d-3}=0\}$ (supremum $0$ if that set is empty or unbounded), $\mathrm{sphereArea}(n)=2\pi^{(n+1)/2}/\Gamma((n+1)/2)$ and $\omega_n=16\pi/(n\,\mathrm{sphereArea}(n))$ .

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. (32): Schwarzschild black-hole entropy S∝M(d−2)/(d−3)S\propto M^{(d-2)/(d-3)}S∝M(d−2)/(d−3)

Eq. (32): Schwarzschild black-hole entropy $S\propto M^{(d-2)/(d-3)}$