Conformal UV divergences and the finite dimensionless remainder

Open

QAlgorithms.Papers.Independent.Intakethird100.P58.conformal_uv_entropy

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

prove2quantum

For the regular conformal disk profiles just described, let $l>0$ be the translation-invariant cylinder length, $N_c\ge1$ the number of colors, $R>0$ the boundary radius, and $b>0$ the axis depth. There is a finite dimensionless number $\widetilde\gamma$ , independent of $R,l,N_c$ and the regular disk representation, such that the actual reduced action

S(a)=\frac{4N_c^2l}{15\pi}\int_a^b\frac{r(z)}{z^3}\sqrt{1+r'(z)^2}\,dz

satisfies, as $a\to0^+$ ,

S(a)-\frac{2N_c^2}{15\pi}\left(\frac{lR}{a^2}+\frac{l}{4R}\log\frac aR\right) \longrightarrow-\frac{4N_c^2l}{15\pi R}\widetilde\gamma.

The integral includes the side surface only. This isolates a finite conformal remainder without promoting the numerical report $0.305$ to an exact equality.

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.9, (3.15): actual conformal profile integral minus both UV terms
has a finite limit. The dimensionless remainder is independent of R,l,N.
The numerical estimate 0.305 is not promoted to an exact equality. -/
theorem conformal_uv_entropy :
    ∃ gamma : ℝ, ∀ (R b : ℝ) (r : ℝ → ℝ), IsDisk .conformal R b r →
      ∀ (l : ℝ), 0 < l → ∀ N : ℕ, 0 < N →
        Tendsto (fun a => conformalEntropy N l r a b -
          4 * (N : ℝ) ^ 2 * l / (15 * Real.pi) * uv .conformal R a)
          (nhdsWithin (0 : ℝ) (Ioi 0))
          (nhds (-4 * (N : ℝ) ^ 2 * l / (15 * Real.pi * R) * gamma)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P58

end

Source

Topological Entanglement Entropy and Holography, arXiv:0805.1891v2, PDF p. 9, (3.13)–(3.15)

Read-back

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

There exists a real constant $\gamma$ such that the following holds for every pair of real numbers $R,b$ and every function $r:\mathbb R\to\mathbb R$ satisfying these conditions: $R>0$ , $b>0$ , $r(0)=R$ , $r$ is continuous and strictly decreasing on $[0,b]$ , $r$ is twice continuously differentiable at every point of $[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$ is required to be Lebesgue interval-integrable from $a$ to $b$ . It is also required that $r(b)=0$ and that

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

with value $0$ for an empty set, be twice continuously differentiable within $[0,R)$ and have derivative $0$ at $0$ within $[0,\infty)$ . For every real $l>0$ and every natural number $N>0$ , these hypotheses imply

\lim_{a\to0^+} \frac{4N^2l}{15\pi} \left[ \int_a^b \frac{r(z)}{z^3}\sqrt{1+r'(z)^2}\,dz -\left(\frac{R}{2a^2}+\frac{\log(a/R)}{8R}\right) \right] = -\frac{4N^2l}{15\pi R}\,\gamma.

The same $\gamma$ is used for all such $R,b,r,l,N$ ; $N=0$ and $l\leq0$ are excluded by the hypotheses.

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