Eq. (30): CFT entropy grows like $E^{(d-1)/d}$

Proved

GravityNonRenorm.cft_entropy_exponent_eq30

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

black-holesquantum-gravity

Let $d\ge 2$ and $a,b,R>0$ , and let $S_{\rm CFT}(E)=a\bigl(R\,(E/(bR^{d-1}))^{1/d}\bigr)^{d-1}$ be the entropy, as a function of energy, of a $d$ -dimensional CFT on $\mathbb R\times S^{d-1}$ obeying Eq. (29). Then, as $E\to\infty$ ,

S_{\rm CFT}(E)=\Theta\!\left(E^{\frac{d-1}{d}}\right),

i.e. $S_{\rm CFT}(E)$ is bounded above and below by positive constant multiples of $E^{(d-1)/d}$ for all sufficiently large $E$ . This is the precise content of the paper's $S\sim E^{(d-1)/d}$ .

Preamble

import Definitions.Def_GravityNonRenorm_Defs
import Mathlib

open GravityNonRenorm Filter Asymptotics

Formal statement

namespace GravityNonRenorm
theorem cft_entropy_exponent_eq30 (d : ℕ) (hd : 2 ≤ d) (a b R : ℝ) (ha : 0 < a) (hb : 0 < b)
    (hR : 0 < R) :
    (fun E : ℝ => cftEntropyOfEnergy d a b R E) =Θ[atTop]
      (fun E : ℝ => E ^ (((d : ℝ) - 1) / d)) := 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\ge 2$ and all reals $a,b,R>0$ , the function $E\mapsto \mathrm{cftEntropyOfEnergy}(d,a,b,R,E)$ (on $\mathbb R$ ) is $\Theta$ of the function $E\mapsto E^{(d-1)/d}$ as $E\to+\infty$ , where $(d-1)/d$ is computed in the reals (with $d$ cast to a real) and the power is a real power. 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. (30): CFT entropy grows like E(d−1)/dE^{(d-1)/d}E(d−1)/d

Eq. (30): CFT entropy grows like $E^{(d-1)/d}$