Eq. (29): CFT entropy–energy relation inverts the thermal relations

Proved

GravityNonRenorm.cft_entropy_energy_eq29

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

black-holesquantum-gravity

Let $d\ge 2$ be the spacetime dimension of a conformal field theory on $\mathbb R_{\rm time}\times S^{d-1}$ , with sphere radius $R>0$ , energy coefficient $b>0$ and any entropy coefficient $a$ . 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. Then for every temperature $T>0$ ,

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

That is, evaluating the entropy function at the thermal energy $E=bR^{d-1}T^d$ of Eq. (29) returns the thermal entropy $S=a(RT)^{d-1}$ of Eq. (29). This certifies that the mission's CFT entropy function is exactly the elimination of $T$ from Eq. (29).

Preamble

import Definitions.Def_GravityNonRenorm_Defs
import Mathlib

open GravityNonRenorm Filter Asymptotics

Formal statement

namespace GravityNonRenorm
theorem cft_entropy_energy_eq29 (d : ℕ) (hd : 2 ≤ d) (a b R T : ℝ) (hb : 0 < b) (hR : 0 < R)
    (hT : 0 < T) :
    cftEntropyOfEnergy d a b R (b * R ^ (d - 1) * T ^ d) = a * (R * T) ^ (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$ with $d\ge 2$ and all real numbers $a,b,R,T$ with $b>0$ , $R>0$ , $T>0$ ( $a$ is unrestricted), the statement asserts

\mathrm{cftEntropyOfEnergy}\bigl(d,a,b,R,\ b\,R^{d-1}T^{d}\bigr)=a\,(RT)^{d-1},

where $d-1$ is natural-number subtraction (exact since $d\ge2$ ) and all displayed powers have natural-number exponents. Unfolding the definition, the left side is $a\cdot\bigl(R\cdot(bR^{d-1}T^d/(bR^{d-1}))^{1/d}\bigr)^{d-1}$ with $1/d$ a real exponent.

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