Regular D3 cylinder endpoint expansion

Open

QAlgorithms.Papers.Independent.Intakethird100.P58.d3_tip_expansion

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

prove2quantum

In the dimensionless compactified D3 reduced model, fix an endpoint radius $r_0>0$ . There exists a regular cylinder profile $r:[0,1]\to\mathbb R$ anchored at the boundary $z=0$ , with $r(1)=r_0$ , satisfying the Euler–Lagrange equation of $\int r z^{-3}\sqrt{1+(1-z^4)r'^2}\,dz$ . Its regulated areas are finite and

r(z)=r_0+\frac{1-z}{4r_0}+o(1-z),\qquad z\to1^-.

This supplies regular endpoint data for the shooting family. The singular joining limit $r_0=0$ is excluded.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P58

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P58

open Set Filter MeasureTheory

open scoped Topology

/-- PDF p.11, (3.20)--(3.21): regular D3 cylinders exist and have the
stated endpoint expansion. The divided formula excludes the singular r0=0 limit. -/
theorem d3_tip_expansion (r0 : ℝ) (hr0 : 0 < r0) :
    ∃ r : ℝ → ℝ, IsCylinder .d3 (r 0) r ∧ r 1 = r0 ∧
      Asymptotics.IsLittleO (nhdsWithin (1 : ℝ) (Iio 1))
        (fun z => r z - r0 - (1 - z) / (4 * r0)) (fun z => 1 - z) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P58

end

Source

Topological Entanglement Entropy and Holography, arXiv:0805.1891v2, PDF p. 11, (3.20)–(3.21)

Read-back

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

For every real $r_0>0$ , there exists a function $r:\mathbb R\to\mathbb R$ with $r(1)=r_0$ satisfying the following conditions: $r(0)>0$ , $r$ is continuous and strictly decreasing on $[0,1]$ , $r$ is twice continuously differentiable at every point of $[0,1]$ as a function on $\mathbb R$ , and for every $z\in(0,1)$ ,

r(z)>0,\qquad \left.\frac{d}{du} \left( \frac{r(u)(1-u^4)r'(u)} {u^3\sqrt{1+(1-u^4)r'(u)^2}} \right)\right|_{u=z} = \frac{\sqrt{1+(1-z^4)r'(z)^2}}{z^3}.

For every real $a$ with $0<a<1$ , the function

z\longmapsto \frac{r(z)}{z^3}\sqrt{1+(1-z^4)r'(z)^2}

is Lebesgue interval-integrable from $a$ to $1$ . This function $r$ also satisfies

r(z)-r_0-\frac{1-z}{4r_0}=o(1-z) \qquad(z\to1^-),

meaning that the absolute value of the displayed remainder divided by $|1-z|$ tends to $0$ .

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