D4 regular tip expansion and its actual inverse

Open

QAlgorithms.Papers.Independent.Intakethird100.P58.d4_tip_expansion

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

prove2quantum

In the dimensionless D4 reduced model, fix $r_0>0$ . There exists a regular cylinder inverse profile $r(z)$ solving the variational equation of $\int r^2z^{-3}\sqrt{1+z(1-z^3)r'^2}\,dz$ , with $r(1)=r_0$ . Let $z(t)$ be the actual inverse on the range of this strictly decreasing graph. Then

r(z)=r_0+\frac{2}{3r_0}(1-z)+o(1-z)\quad(z\to1^-),

and

z(t)=1-\frac32r_0(t-r_0)+o(t-r_0)\quad(t\to r_0^+).

The two slopes are reciprocal, and the zero-radius singular joining limit is excluded. These formulas are regular tip data, not entropy-minimality statements.

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.16, (4.13)--(4.14): the D4 tip expansion and the reciprocal
expansion of its actual inverse. The endpoint radius is positive. -/
theorem d4_tip_expansion (r0 : ℝ) (hr0 : 0 < r0) :
    ∃ r : ℝ → ℝ, IsCylinder .d4 (r 0) r ∧ r 1 = r0 ∧
      Asymptotics.IsLittleO (nhdsWithin (1 : ℝ) (Iio 1))
        (fun z => r z - r0 - 2 * (1 - z) / (3 * r0)) (fun z => 1 - z) ∧
      Asymptotics.IsLittleO (nhdsWithin r0 (Ioi r0))
        (fun t => height r 1 t - 1 + (3 : ℝ) / 2 * r0 * (t - r0))
        (fun t => t - r0) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P58

end

Source

Topological Entanglement Entropy and Holography, arXiv:0805.1891v2, PDF p. 16, (4.13)–(4.14)

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 these 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)^2u(1-u^3)r'(u)} {u^3\sqrt{1+u(1-u^3)r'(u)^2}} \right)\right|_{u=z} = \frac{2r(z)}{z^3}\sqrt{1+z(1-z^3)r'(z)^2}.

For every real $a$ with $0<a<1$ , the function $z\mapsto r(z)^2\sqrt{1+z(1-z^3)r'(z)^2}/z^3$ is Lebesgue interval-integrable from $a$ to $1$ . Defining

H(t)=\inf\{z\in[0,1]:r(z)=t\},

with value $0$ if the set is empty, the two asserted expansions are

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

and

H(t)-1+\frac32r_0(t-r_0)=o(t-r_0) \qquad(t\to r_0^+).

In each expansion, the absolute value of the remainder divided by the absolute value of the indicated comparison function 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