Provedads-cfthep-th-9802150sign-auditthermal-ads
With t = ln v − ½ ln(1 + r²) the quotient embedding u = e^{−t}√(1+r²), v = e^{t}√(1+r²) induces the metric components (1 + r², 0, 1/(1 + r²))
For all :
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- t, r range over real numbers: the statement must hold for every choice. (
(t r : ℝ)) - f′(x)Derivative
- The derivative of s ↦ exp(−s) · √(1 + r^2) at t: its instantaneous rate of change there. (
deriv (fun s : ℝ => Real.exp (-s) * Rea…) - =Equality
- deriv(s ↦ exp(−s) · √(1 + r^2), t) · deriv(s ↦ exp(s) · √(… and −(1 + r^2) are the same. (
deriv (fun s : ℝ => Real.exp (-s) * Rea…) - x ↦ f(x)Function (λ-abstraction)
- The function sending s to exp(−s) · √(1 + r^2). Lean writes fun x => …; papers write x ↦ …. (
fun s : ℝ => Real.exp (-s) * Real.sqrt …) - eˣExponential function
- e raised to the power −s, where e ≈ 2.718. (
Real.exp (-s)) - ·Multiplication
- exp(−s) times √(1 + r^2). (
Real.exp (-s) * Real.sqrt (1 + r ^ 2)) - −xNegation
- The negative of s. (
-s) - √Square root
- The non-negative number whose square is 1 + r^2. (
Real.sqrt (1 + r ^ 2)) - +Addition
- 1 plus r^2. (
1 + r ^ 2) - aᵇPower
- r raised to the power 2. (
r ^ 2) - ∧And
- Both hold: deriv(s ↦ exp(−s) · √(1 + r^2), t) · deriv(ρ ↦ exp(t) · √(…, and 1 − deriv(ρ ↦ exp(−t) · √(1 + ρ^2), r) · deriv(ρ ↦ exp(t) …. (
deriv (fun s : ℝ => Real.exp (-s) * Rea…) - -Subtraction
- 1 minus deriv(ρ ↦ exp(−t) · √(1 + ρ^2), r) · deriv(ρ ↦ exp(t) · √(…. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - deriv (fun ρ : ℝ => Real.exp (-t) *…) - a/bDivision
- 1 divided by 1 + r^2. In Lean, dividing by 0 gives 0. (
1 / (1 + r ^ 2))
theorem thermal-quotient-time-coordinate-corrected-sign (t r : ℝ) :
deriv (fun s : ℝ => Real.exp (-s) * Real.sqrt (1 + r ^ 2)) t * deriv (fun s : ℝ => Real.exp s * Real.sqrt (1 + r ^ 2)) t = -(1 + r ^ 2) ∧ deriv (fun s : ℝ => Real.exp (-s) * Real.sqrt (1 + r ^ 2)) t * deriv (fun ρ : ℝ => Real.exp t * Real.sqrt (1 + ρ ^ 2)) r + deriv (fun ρ : ℝ => Real.exp (-t) * Real.sqrt (1 + ρ ^ 2)) r * deriv (fun s : ℝ => Real.exp s * Real.sqrt (1 + r ^ 2)) t = 0 ∧ 1 - deriv (fun ρ : ℝ => Real.exp (-t) * Real.sqrt (1 + ρ ^ 2)) r * deriv (fun ρ : ℝ => Real.exp t * Real.sqrt (1 + ρ ^ 2)) r = 1 / (1 + r ^ 2)Thermal anti-de Sitter space as the quotient of the quadric uv - r^2 = 1 (hep-th/9802150 section 3.2, eqs. 3.5-3.12) with ambient form -du dv + dr^2 + r^2 dOmega^2. The paper writes t = ln v + (1/2) ln(1 + r^2); with that sign the induced metric has a cross term -2r dt dr (statement thermal-quotient-time-coordinate-printed-sign). With t = ln v - (1/2) ln(1 + r^2), i.e. u = e^{-t} sqrt(1+r^2), v = e^{t} sqrt(1+r^2), the components are g_tt = -u_t v_t = 1 + r^2, g_tr = -(u_t v_r + u_r v_t)/2 = 0, g_rr = 1 - u_r v_r = 1/(1 + r^2): eq. (3.12). Stated with Mathlib's deriv of the explicit functions. Decided in Alpha as wittonPullbackCrossLaw and wittonPullbackRadialLaw (Witton.QuotientTimePullback).
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
- 48 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.