A finite exterior BTZ geodesic turns before the horizon

Open

QAlgorithms.Papers.Independent.Intakethird100.P26.btz_geodesic_turns_before_horizon

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $l,r_+,\rho_0>0$ . On a constant Euclidean-time slice of the nonextremal BTZ geometry, use the spatial metric

ds^2=d\rho^2+r_+^2\cosh^2(\rho/l)\,d\phi^2,\qquad \phi\sim\phi+2\pi.

Let $x(t)=(\rho(t),\phi(t))$ , $a\le t\le b$ with $a<b$ , be an affinely parameterized $C^2$ geodesic, using one fixed angular lift. Suppose $0\le\rho(t)\le\rho_0$ , both endpoint radii equal $\rho_0$ , and the endpoint angles represent distinct points modulo $2\pi$ . Then there is an interior turning point $t_*$ at which

0<\rho(t_*)<\rho_0,\qquad \dot\rho(t_*)=0,\qquad \rho(t_*)\le\rho(t)\quad(a\le t\le b).

Thus this finite exterior geodesic stays away from the horizon. Its geodesic predicate is the Euler–Lagrange equation of the displayed metric’s kinetic energy; it does not assume the turning property.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P26

Formal statement

noncomputable section

open Set

namespace QAlgorithms.Papers.Independent.Intakethird100.P26

/-- PDF p.9, following (2.13) on p.8: a finite nonconstant constant-tau
exterior BTZ geodesic between distinct cutoff-circle endpoints turns strictly
before the horizon. A lift fixes the winding; distinctness is on the actual
angular circle. The permitted radial domain includes the horizon, so strict
positivity of the turning radius is a conclusion. No entropy identity is used. -/
theorem btz_geodesic_turns_before_horizon
    (l rplus rho0 a b : ℝ) (hl : 0 < l) (hrplus : 0 < rplus)
    (hrho0 : 0 < rho0) (hab : a < b)
    (x : ℝ → (Fin 2 → ℝ))
    (hgeo : IsBTZSliceGeodesic l rplus a b x)
    (hcutoff : ∀ t ∈ Icc a b, 0 ≤ x t 0 ∧ x t 0 ≤ rho0)
    (hstart : x a 0 = rho0) (hend : x b 0 = rho0)
    (hdistinct : (↑(x a 1) : AddCircle (2 * Real.pi)) ≠
      (↑(x b 1) : AddCircle (2 * Real.pi))) :
    ∃ t ∈ Ioo a b,
      0 < x t 0 ∧ x t 0 < rho0 ∧ deriv (fun s => x s 0) t = 0 ∧
        ∀ s ∈ Icc a b, x t 0 ≤ x s 0 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P26

end

Source

Proof of the Holographic Formula for Entanglement Entropy, arXiv:hep-th/0606184v2, PDF p. 9, Section 2, following (2.13)

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every choice of real numbers $l,r_+,\rho_0,a,b$ satisfying $l>0$ , $r_+>0$ , $\rho_0>0$ , and $a<b$ , and every function $x:\mathbb R\to\mathbb R^2$ , suppose that $x$ is twice continuously differentiable within $[a,b]$ and, for every $t\in(a,b)$ and $j\in\{0,1\}$ , satisfies

\left.\frac{d}{ds}\left(D_vE_{l,r_+}(x(s),x'(s))[e_j]\right)\right|_{s=t} = D_qE_{l,r_+}(x(t),x'(t))[e_j], \qquad E_{l,r_+}(q,v)=\frac{v_0^2+r_+^2\cosh^2(q_0/l)\,v_1^2}{2},

where $e_j$ is the $j$ -th coordinate vector and $D_v,D_q$ are derivatives in the indicated arguments. Suppose also that $0\le x_0(t)\le\rho_0$ for every $t\in[a,b]$ , that $x_0(a)=x_0(b)=\rho_0$ , and that $x_1(a)$ and $x_1(b)$ represent distinct elements of the additive quotient $\mathbb R/(2\pi\mathbb Z)$ . Then there exists $t\in(a,b)$ such that

0<x_0(t)<\rho_0,\qquad \left.\frac{d}{ds}x_0(s)\right|_{s=t}=0,\qquad x_0(t)\le x_0(s)\quad\text{for every }s\in[a,b].

Thus the asserted point attains a minimum over the entire closed interval; neither the point nor the minimum is asserted to be unique.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph