proofs
Provedads-cftblack-hole-thermodynamicshep-th-9802150hep-th-9803131

The area law βM − I = S of the Schwarzschild–anti-de Sitter black hole in n+1 dimensions, as a rational identity in the horizon radius

For all n∈N\htmlData{mx=1}{n \in \htmlData{mx=0}{\mathbb{N}}} and r∈R\htmlData{mx=1}{r \in \htmlData{mx=0}{\mathbb{R}}}, if 2≤n2 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{n} and 0<r0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{r}, then

4rn⋅r2+n−2⋅((n−1)⋅(rn−2+rn)16)−rn−1−rn+14(n⋅r2+n−2)=rn−14\begin{aligned} & \htmlData{mx=45}{\htmlData{mx=25}{\htmlData{mx=11}{\frac{\htmlData{mx=2}{4\htmlData{mx=1}{r}}}{\htmlData{mx=10}{\htmlData{mx=9}{\htmlData{mx=7}{\htmlData{mx=4}{\htmlData{mx=3}{n}} \cdot \htmlData{mx=6}{\htmlData{mx=5}{r}^{2}}} + \htmlData{mx=8}{n}} - 2}}} \cdot \left(\htmlData{mx=24}{\frac{\htmlData{mx=23}{(\htmlData{mx=14}{\htmlData{mx=13}{\htmlData{mx=12}{n}} - 1}) \cdot (\htmlData{mx=22}{\htmlData{mx=18}{\htmlData{mx=15}{r}^{\htmlData{mx=17}{\htmlData{mx=16}{n} - 2}}} + \htmlData{mx=21}{\htmlData{mx=19}{r}^{\htmlData{mx=20}{n}}}})}}{16}}\right)} - \htmlData{mx=44}{\frac{\htmlData{mx=34}{\htmlData{mx=29}{\htmlData{mx=26}{r}^{\htmlData{mx=28}{\htmlData{mx=27}{n} - 1}}} - \htmlData{mx=33}{\htmlData{mx=30}{r}^{\htmlData{mx=32}{\htmlData{mx=31}{n} + 1}}}}}{\htmlData{mx=43}{4(\htmlData{mx=42}{\htmlData{mx=41}{\htmlData{mx=39}{\htmlData{mx=36}{\htmlData{mx=35}{n}} \cdot \htmlData{mx=38}{\htmlData{mx=37}{r}^{2}}} + \htmlData{mx=40}{n}} - 2})}}}} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=50}{\frac{\htmlData{mx=49}{\htmlData{mx=46}{r}^{\htmlData{mx=48}{\htmlData{mx=47}{n} - 1}}}}{4}} \end{aligned}
What the notation means · or point at any symbol
NNatural numbers
The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
≤At most
2 is less than or equal to n. (2 ≤ n)
RReal numbers
The real numbers: every point on the number line. (ℝ)
<Less than
0 is strictly smaller than r. (0 < r)
·Multiplication
4 times r. (4 * r)
a/bDivision
4 · r divided by n · r^2 + n − 2. In Lean, dividing by 0 gives 0. (4 * r / ((n : ℝ) * r ^ 2 + n - 2))
=Equality
4 · r/(n · r^2 + n − 2) · ((n − 1) · (r^(n − 2) + r^n)/16)… and r^(n − 1)/4 are the same. (4 * r / ((n : ℝ) * r ^ 2 + n - 2) * (((…)
(x : T)As real numbers
n read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((n : ℝ))
+Addition
n · r^2 plus n. ((n : ℝ) * r ^ 2 + n)
-Subtraction
n · r^2 + n minus 2. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. ((n : ℝ) * r ^ 2 + n - 2)
aᵇPower
r raised to the power 2. (r ^ 2)

With unit curvature radius and Vol(S^{n-1}), Newton's constant and pi divided out: the regular period is beta = 4 r / (n r^2 + n - 2) (Witten hep-th/9803131 eq. 2.9; for n = 3 the corrected eq. 3.15 of hep-th/9802150, which prints 12 pi for 4 pi), the mass is M = (n-1)(r^{n-2} + r^n)/16, the action difference I = (r^{n-1} - r^{n+1})/(4(n r^2 + n - 2)) (hep-th/9803131 eq. 2.18) and the entropy S = r^{n-1}/4 (a quarter of the horizon area). This statement is beta M - I = S for every n >= 2 and r > 0. The first law dI/dbeta = M is the companion statement, decided symbolically in Alpha (wittonGeneralFirstLawLaw) and not posed here. Decided in Alpha as wittonGeneralAreaLaw (Witton.GeneralDimensionThermodynamics).

How it was proved

Proved
17 October 2026
By
Ajax
Checked by
Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms
Classical.choice, Quot.sound, propext
Proof
27 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements