Conformal boundary profile and its finite-order logarithmic expansion

Open

QAlgorithms.Papers.Independent.Intakethird100.P58.conformal_uv_profile

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

prove2quantum

Consider a regular rotational disk profile in the conformal reduced model, with boundary-cylinder radius $R>0$ and maximal depth $b>0$ . Write $z(t)$ for the direct graph, $r(z)$ for its inverse, $x=1-t/R$ , and $f(x)=z(R(1-x))/(2R\sqrt{x})$ . The graphs satisfy the Euler–Lagrange equation of $\int r z^{-3}\sqrt{1+r'^2}\,dz$ , the regular axis condition, and positive finite regulated area. Such regular disks exist for every $R>0$ . There are universal functions $B_1,B_2,B_3$ of one real variable such that each disk has a coefficient $a_1\in\mathbb R$ with

z(t)\sim2\sqrt{R}\sqrt{R-t},\qquad f(x)=1+a_1x+\tfrac18x\log x+\sum_{j=0}^{2} B_{j+1}(a_1)x^2(\log x)^j+o(x^2),

and

r(z)=R-\frac{z^2}{4R}+O(z^4\log z).

All limits approach the boundary from the physical interior. This identifies the local terms that control the conformal UV subtraction; it asserts no convergence of an infinite formal series.

Formalization Note The printed variable $1-R/t$ is corrected to $1-t/R$ , as required by the real square root and the displayed ODE. The coordinate correction was independently checked against (3.8)–(3.10) and (3.14) in moderation round one.

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 pp.7--9, (3.8)--(3.11),(3.14): finite-order conformal boundary
asymptotics of the regular disk profile. The printed x=1-R/r is corrected to
x=1-r/R because (3.8),(3.9),(3.10),(3.14) require positive x in the interior.
The three second-order coefficients depend only on a1, and no convergence of
an infinite formal series is asserted. The coordinate correction is fixed by
these source equations. -/
theorem conformal_uv_profile :
    ∃ B1 B2 B3 : ℝ → ℝ,
      (∀ R : ℝ, 0 < R → ∃ b : ℝ, ∃ r : ℝ → ℝ, IsDisk .conformal R b r) ∧
      ∀ (R b : ℝ) (r : ℝ → ℝ), IsDisk .conformal R b r →
        (Tendsto (fun t => height r b t /
          (2 * Real.sqrt R * Real.sqrt (R - t)))
          (nhdsWithin R (Iio R)) (nhds 1)) ∧
        (∃ a1 : ℝ,
          Asymptotics.IsLittleO (nhdsWithin (0 : ℝ) (Ioi 0))
            (fun x => conformalF R b r x -
              (1 + a1 * x + x * Real.log x / 8 + B1 a1 * x ^ 2 +
                B2 a1 * x ^ 2 * Real.log x + B3 a1 * x ^ 2 * Real.log x ^ 2))
            (fun x => x ^ 2)) ∧
        Asymptotics.IsBigO (nhdsWithin (0 : ℝ) (Ioi 0))
          (fun z => r z - R + z ^ 2 / (4 * R))
          (fun z => z ^ 4 * Real.log z) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P58

end

Source

Topological Entanglement Entropy and Holography, arXiv:0805.1891v2, PDF p. 7, (3.8)–(3.11), (3.14)

Read-back

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

There exist three functions $B_1,B_2,B_3:\mathbb R\to\mathbb R$ , common to all the data below, with the following properties. For every real $R>0$ , there exist a real $b$ and a function $r:\mathbb R\to\mathbb R$ satisfying these disk conditions: $b>0$ , $r(0)=R$ , $r$ is continuous and strictly decreasing on $[0,b]$ , $r$ is twice continuously differentiable at every $z\in[0,b)$ as a function on $\mathbb R$ , and for every $z\in(0,b)$ ,

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

For every real $a$ with $0<a<b$ , the function $z\mapsto r(z)\sqrt{1+r'(z)^2}/z^3$ must be Lebesgue interval-integrable from $a$ to $b$ . The remaining disk conditions are $r(b)=0$ and, on defining

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

that $H$ is twice continuously differentiable within $[0,R)$ and has derivative $0$ at $0$ within $[0,\infty)$ . The infimum defining $H$ is assigned the value $0$ when its set is empty. For every real $R,b$ and every function $r$ satisfying all these disk conditions, including $R>0$ , one has

\lim_{t\to R^-} \frac{H(t)}{2\sqrt R\sqrt{R-t}}=1;

there exists a real $a_1$ , which may depend on $R,b,r$ , such that, as $x\to0^+$ ,

\frac{H(R(1-x))}{2R\sqrt x} -\left( 1+a_1x+\frac{x\log x}{8} +B_1(a_1)x^2 +B_2(a_1)x^2\log x +B_3(a_1)x^2(\log x)^2 \right) =o(x^2);

and, as $z\to0^+$ ,

r(z)-R+\frac{z^2}{4R}=O(z^4\log z).

Here the little- $o$ assertion means that the absolute value of its left-hand side divided by $x^2$ tends to $0$ ; the big- $O$ assertion means that the absolute value of its left-hand side is eventually bounded by a fixed nonnegative constant times $|z^4\log z|$ .

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