Finite UV-subtracted D4 reduced action

Open

QAlgorithms.Papers.Independent.Intakethird100.P58.d4_uv_entropy

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

prove2quantum

Fix positive D4 coupling $\lambda$ and compactification radius $R_4$ , and an integer $N_c\ge1$ , with $\alpha'=1$ . Put $U_0=4\pi\lambda/(9R_4^2)$ , $R_{\mathrm{curv}}^3=\pi\lambda$ , $G_N^{(10)}=8\pi^6\lambda^2/N_c^2$ , and $K=\pi^3R_{\mathrm{curv}}^6U_0R_4/(2G_N^{(10)})$ . For any regular physical disk or cylinder inverse profile $r(z)$ with boundary radius $\rho>0$ and endpoint depth $b$ , use the actual reduced action

S(a)=K\int_a^b\frac{r(z)^2}{z^3}\sqrt{1+z(1-z^3)r'(z)^2}\,dz.

There exists a finite real remainder $S_{\mathrm{finite}}(0)$ such that

S(a)-K\left[\frac{\rho^2}{2a^2}-\frac{3}{2a}+\frac{\log a}{8\rho^2}\right] \longrightarrow S_{\mathrm{finite}}(0)\qquad(a\to0^+).

This is the UV subtraction for the chosen reduced functional. It does not derive its disputed absolute geometric normalization or assert physical validity at arbitrarily high field-theory cutoff.

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.18--19, (4.17): finite UV remainder of the actual reduced D4 action
for either regular topology. K is exactly the chosen reduced-regulatedAction prefactor;
no assertion repairs the induced-metric normalization. -/
theorem d4_uv_entropy (P : D4Parameters) (N : ℕ) (hN : 0 < N)
    (rho b : ℝ) (r : ℝ → ℝ) (hr : IsProfile .d4 rho b r) :
    ∃ finite : ℝ,
      Tendsto (fun a => d4Entropy P N r a b - d4Prefactor P N * uv .d4 rho a)
        (nhdsWithin (0 : ℝ) (Ioi 0)) (nhds finite) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P58

end

Source

Topological Entanglement Entropy and Holography, arXiv:0805.1891v2, PDF p. 18, (4.17)

Read-back

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

For every parameter record $P$ consisting of real numbers $\lambda>0$ and $L>0$ , respectively its coupling and circle radius, every natural number $N>0$ , every pair of real numbers $\rho,b$ , and every function $r:\mathbb R\to\mathbb R$ satisfying the profile conditions below, there exists a real number $F$ giving the stated limit. The common profile conditions are $\rho>0$ , $b>0$ , $r(0)=\rho$ , continuity and strict decrease of $r$ on $[0,b]$ , twice continuous differentiability of $r$ 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)^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<b$ , the function $z\mapsto r(z)^2\sqrt{1+z(1-z^3)r'(z)^2}/z^3$ must be Lebesgue interval-integrable from $a$ to $b$ . In addition, at least one of two alternatives must hold: either $b<1$ , $r(b)=0$ , and

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

with value $0$ for an empty set, is twice continuously differentiable within $[0,\rho)$ and has derivative $0$ at $0$ within $[0,\infty)$ ; or $b=1$ , $r(1)>0$ , and $r$ is twice continuously differentiable at $1$ as a function on $\mathbb R$ . Define the real prefactor

K= \frac{ \pi^3(\pi\lambda)^2 \left(\frac{4\pi\lambda}{9L^2}\right)L }{ 2\left(\frac{8\pi^6\lambda^2}{N^2}\right) }.

The conclusion is that some $F\in\mathbb R$ , allowed to depend on all these data, satisfies

\lim_{a\to0^+} K\left[ \int_a^b \frac{r(z)^2}{z^3}\sqrt{1+z(1-z^3)r'(z)^2}\,dz -\left( \frac{\rho^2}{2a^2} -\frac{3}{2a} +\frac{\log a}{8\rho^2} \right) \right] =F.

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