Large-tip D3 cylinder profile

Open

QAlgorithms.Papers.Independent.Intakethird100.P58.d3_large_tip_expansion

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

prove2quantum

There exist a family $r_t(z)$ of regular dimensionless D3 cylinder profiles, with $t>0$ , $r_t(1)=t$ , and boundary radius $r_t(0)$ , and a function $f\in C^1([0,1])$ with $f(1)=0$ , such that for every fixed $0<a<1$ ,

r_t(z)=t+\frac{f(z)}t+o(t^{-1})\qquad(t\to\infty)

uniformly for $z\in[a,1]$ . Equivalently, for every $\epsilon>0$ there is $T>0$ , independent of $t$ and $z$ , for which $|t(r_t(z)-t)-f(z)|\le\epsilon$ whenever $t\ge T$ and $a\le z\le1$ .

Every member solves the source Euler–Lagrange equation and has finite positive-cutoff area; the asymptotic expansion is derived as a conclusion. This describes approach to a straight cylinder on regulated intervals. It does not identify the entropy-minimizing branch.

The boundary value is included separately: $t(r_t(0)-t)\to f(0)$ as $t\to\infty$ , so $R_t=r_t(0)=t+f(0)/t+o(t^{-1})$ . This is the boundary-radius consequence used in passing from (3.22) to (3.24).

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.22): construct the regular D3 cylinder family and its large-tip
correction, including R=r(0)=r0+f(0)/r0+o(1/r0) at the boundary.
The o(1/r0) estimate is uniform on each fixed compact regulated z interval. The reference to solving (3.21) means the ODE (3.20) with that
endpoint data. No large-radius expansion is assumed as a premise. -/
theorem d3_large_tip_expansion :
    ∃ (C : ℝ → ℝ → ℝ) (f : ℝ → ℝ),
      (∀ t : ℝ, 0 < t → IsCylinder .d3 (C t 0) (C t) ∧ C t 1 = t) ∧
      f 1 = 0 ∧ (∀ z ∈ Icc (0 : ℝ) 1, ContDiffAt ℝ 1 f z) ∧
      Tendsto (fun t => t * (C t 0 - t)) atTop (nhds (f 0)) ∧
      ∀ a : ℝ, 0 < a → a < 1 → ∀ epsilon : ℝ, 0 < epsilon →
        ∃ T : ℝ, 0 < T ∧ ∀ t : ℝ, T ≤ t →
          ∀ z ∈ Icc a 1, |t * (C t z - t) - f z| ≤ epsilon := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P58

end

Source

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

Read-back

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

There exist functions $C:\mathbb R\times\mathbb R\to\mathbb R$ and $f:\mathbb R\to\mathbb R$ , writing $C_t(z)=C(t,z)$ , with the following properties. For every real $t>0$ , $C_t(0)>0$ , $C_t(1)=t$ , and $C_t$ is continuous and strictly decreasing on $[0,1]$ and is twice continuously differentiable at every point of $[0,1]$ , including both endpoints in the ambient real line. For every $z\in(0,1)$ , $C_t(z)>0$ and

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

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

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

is interval integrable with respect to Lebesgue measure from $a$ to $1$ . The function $f$ satisfies $f(1)=0$ and is once continuously differentiable at every point of $[0,1]$ , again in the ambient real line. Moreover,

\lim_{t\to+\infty}t\bigl(C_t(0)-t\bigr)=f(0),

and for every real $a$ with $0<a<1$ and every real $\varepsilon>0$ , there exists a real $T>0$ such that, for every real $t\ge T$ and every $z\in[a,1]$ ,

\left|t\bigl(C_t(z)-t\bigr)-f(z)\right|\le\varepsilon.

Thus the latter estimate includes $z=1$ but excludes $z=0$ , where convergence is asserted separately; the cylinder requirements apply only to positive $t$ .

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