Prove2Me

Footnote 26: (d−1)/d<1<(d−2)/(d−3)(d-1)/d<1<(d-2)/(d-3)

Proved
GravityNonRenorm.exponent_comparison_footnote26

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

black-holesquantum-gravity

For every spacetime dimension d≥4d\ge4,

d−1d<1<d−2d−3.\frac{d-1}{d}<1<\frac{d-2}{d-3}.

The left exponent is the CFT entropy exponent of Eq. (30); the right one is the Schwarzschild black-hole entropy exponent of Eq. (32). In particular the two exponents differ, which is the arithmetic core of the non-renormalizability argument.

Preamble
import Definitions.Def_GravityNonRenorm_Defs
import Mathlib

open GravityNonRenorm Filter Asymptotics
Formal statement
namespace GravityNonRenorm
theorem exponent_comparison_footnote26 (d : ℕ) (hd : 4 ≤ d) :
    ((d : ℝ) - 1) / d < 1 ∧ 1 < ((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 dd with d≥4d\ge4, with dd regarded as a real number and real division: (d−1)/d<1(d-1)/d<1 and 1<(d−2)/(d−3)1<(d-2)/(d-3). Both inequalities are strict and asserted simultaneously.

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