Provedads-cfthep-th-9802150sign-auditthermal-ads

With the printed t = ln v + ½ ln(1 + r²) the induced cross component is g_tr = −2r

For all $\htmlData{mx=1}{t, r \in \htmlData{mx=0}{\mathbb{R}}}$ :

\begin{aligned} & \htmlData{mx=59}{\frac{\htmlData{mx=58}{-\left(\htmlData{mx=57}{\htmlData{mx=28}{\htmlData{mx=16}{\htmlData{mx=14}{s \mapsto \htmlData{mx=12}{\htmlData{mx=3}{e^{\htmlData{mx=2}{-\htmlData{mx=1}{s}}}} \cdot \left(\htmlData{mx=11}{(\htmlData{mx=6}{1 + \htmlData{mx=5}{\htmlData{mx=4}{r}^{2}}}) \cdot \htmlData{mx=10}{\sqrt{\htmlData{mx=9}{1 + \htmlData{mx=8}{\htmlData{mx=7}{r}^{2}}}}}}\right)}}'(\htmlData{mx=15}{t})} \cdot \htmlData{mx=27}{\htmlData{mx=25}{\rho \mapsto \htmlData{mx=23}{\frac{\htmlData{mx=18}{e^{\htmlData{mx=17}{t}}}}{\htmlData{mx=22}{\sqrt{\htmlData{mx=21}{1 + \htmlData{mx=20}{\htmlData{mx=19}{\rho}^{2}}}}}}}}'(\htmlData{mx=26}{r})}} + \htmlData{mx=56}{\htmlData{mx=44}{\htmlData{mx=42}{\rho \mapsto \htmlData{mx=40}{\htmlData{mx=31}{e^{\htmlData{mx=30}{-\htmlData{mx=29}{t}}}} \cdot \left(\htmlData{mx=39}{(\htmlData{mx=34}{1 + \htmlData{mx=33}{\htmlData{mx=32}{\rho}^{2}}}) \cdot \htmlData{mx=38}{\sqrt{\htmlData{mx=37}{1 + \htmlData{mx=36}{\htmlData{mx=35}{\rho}^{2}}}}}}\right)}}'(\htmlData{mx=43}{r})} \cdot \htmlData{mx=55}{\htmlData{mx=53}{s \mapsto \htmlData{mx=51}{\frac{\htmlData{mx=46}{e^{\htmlData{mx=45}{s}}}}{\htmlData{mx=50}{\sqrt{\htmlData{mx=49}{1 + \htmlData{mx=48}{\htmlData{mx=47}{r}^{2}}}}}}}}'(\htmlData{mx=54}{t})}}}\right)}}{2}} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=62}{\htmlData{mx=60}{-2} \cdot \htmlData{mx=61}{r}} \end{aligned}

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 : ℝ))
=Equality: −(deriv(s ↦ exp(−s) · ((1 + r^2) · √(1 + r^2)), t) · deriv… and −2 · r are the same. (-(deriv (fun s : ℝ => Real.exp (-s) * (…)
f′(x)Derivative: The derivative of s ↦ exp(−s) · ((1 + r^2) · √(1 + r^2)) at t: its instantaneous rate of change there. (deriv (fun s : ℝ => Real.exp (-s) * ((1…)
x ↦ f(x)Function (λ-abstraction): The function sending s to exp(−s) · ((1 + r^2) · √(1 + r^2)). Lean writes fun x => …; papers write x ↦ …. (fun s : ℝ => Real.exp (-s) * ((1 + r ^ …)
eˣExponential function: e raised to the power −s, where e ≈ 2.718. (Real.exp (-s))
−xNegation: The negative of s. (-s)
·Multiplication: 1 + r^2 times √(1 + r^2). ((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)
√Square root: The non-negative number whose square is 1 + r^2. (Real.sqrt (1 + r ^ 2))
a/bDivision: exp(t) divided by √(1 + ρ^2). In Lean, dividing by 0 gives 0. (Real.exp t / Real.sqrt (1 + ρ ^ 2))

theorem thermal-quotient-time-coordinate-printed-sign (t r : ℝ) :
    -(deriv (fun s : ℝ => Real.exp (-s) * ((1 + r ^ 2) * Real.sqrt (1 + r ^ 2))) t * deriv (fun ρ : ℝ => Real.exp t / Real.sqrt (1 + ρ ^ 2)) r + deriv (fun ρ : ℝ => Real.exp (-t) * ((1 + ρ ^ 2) * Real.sqrt (1 + ρ ^ 2))) r * deriv (fun s : ℝ => Real.exp s / Real.sqrt (1 + r ^ 2)) t) / 2 = -2 * r

The sign printed before eq. (3.12) of hep-th/9802150, t = ln v + (1/2) ln(1 + r^2), corresponds to v = e^{t}/sqrt(1+r^2), u = e^{-t}(1+r^2)^{3/2}; the induced cross component -(u_t v_r + u_r v_t)/2 is then -2r, so (3.12) does not follow from the printed coordinate (it follows from the corrected one, statement thermal-quotient-time-coordinate-corrected-sign). Decided in Alpha as wittonPullbackCrossLaw at sigma = -1 and checked numerically (g_tr = -1.4 at r = 0.7).

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: 64 lines of Lean

With the printed t = ln v + ½ ln(1 + r²) the induced cross component is g_tr = −2r

How it was proved

More proved statements