Large-ball reduced entropy and its exact constant-term integral

Open

QAlgorithms.Papers.Independent.Intakethird100.P58.d4_large_radius_entropy

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

prove2quantum

Fix the positive D4 scales and $N_c\ge1$ as above. There exist $\rho_{\min}>0$ and regular cylinder profiles $r_\rho(z)$ for every $\rho\ge\rho_{\min}$ , anchored by $r_\rho(0)=\rho$ . Let $g$ be the explicit regular coefficient (4.23), put $q(z)=-(1+z)/(1+z+z^2)=g'(z)$ , and define

H(z)=\frac{4g(z)+z(1-z^3)q(z)^2}{2z^3}.

For every fixed regulator $0<a<1$ , $H$ is integrable on $[a,1]$ and the actual reduced entropy satisfies

S(\rho,a)=K\int_a^1\left[\frac{\rho^2}{z^3}+H(z)\right]dz+O(\rho^{-1})\qquad(\rho\to\infty).

Here $K=\pi^3R_{\mathrm{curv}}^6U_0R_4/(2G_N^{(10)})$ is the chosen reduced prefactor, $S_{\rho^2}=K\rho^2\int_a^1z^{-3}dz$ , and $\gamma(a)=-K\int_a^1H(z)dz$ . The error constant and threshold may depend on the fixed regulator and model, and precede $\rho$ .

The result constructs a stationary cylinder family and its area asymptotics without assuming them. It gives the integral coefficient before the disputed evaluations (4.25)/(4.28), and does not exchange the fixed-cutoff and large-radius limits.

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.19--20, (4.24): construct the large-boundary-radius D4 cylinder
family and the constant-term integral of its actual reduced regulatedAction. First fix
0<a<1, then take rho to infinity. Neither a profile expansion nor the resulting
area estimate is assumed. This is the integral coefficient, not (4.25)/(4.28). -/
theorem d4_large_radius_entropy (P : D4Parameters) (N : ℕ) (hN : 0 < N) :
    ∃ (rhoMin : ℝ) (C : ℝ → ℝ → ℝ), 0 < rhoMin ∧
      (∀ rho : ℝ, rhoMin ≤ rho → IsCylinder .d4 rho (C rho)) ∧
      ∀ a : ℝ, 0 < a → a < 1 →
        IntervalIntegrable d4ConstantDensity volume a 1 ∧
        ∃ B M : ℝ, 0 < B ∧ rhoMin ≤ M ∧
          ∀ rho : ℝ, M ≤ rho →
            |d4Entropy P N (C rho) a 1 - d4Prefactor P N *
              (rho ^ 2 * (∫ z in a..(1 : ℝ), 1 / z ^ 3) +
                ∫ z in a..(1 : ℝ), d4ConstantDensity z)| ≤ B / rho := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P58

end

Source

Topological Entanglement Entropy and Holography, arXiv:0805.1891v2, PDF p. 20, (4.24)

Read-back

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

For every parameter pair consisting of real numbers $\kappa>0$ and $L>0$ , representing the coupling and circle radius in $P$ , and every natural number $N>0$ , define

K=\frac{\pi^3(\pi\kappa)^2\left(\frac{4\pi\kappa}{9L^2}\right)L} {2\left(\frac{8\pi^6\kappa^2}{N^2}\right)}, \qquad D_r(z)=\frac{r(z)^2}{z^3}\sqrt{1+z(1-z^3)(r'(z))^2},

and define

G(z)=-\frac{\arctan((1+2z)/\sqrt3)}{\sqrt3} -\frac{\log(1+z+z^2)}2+\frac{\pi}{6\sqrt3}, \qquad H(z)=\frac{4G(z)+z(1-z^3)\left(-\frac{1+z}{1+z+z^2}\right)^2}{2z^3}.

There exist a real number $\rho_{\min}>0$ and a function $C:\mathbb R\to(\mathbb R\to\mathbb R)$ with the following properties. For every real $\rho\ge\rho_{\min}$ , the function $r=C(\rho)$ satisfies $r(0)=\rho$ , is continuous and strictly decreasing on $[0,1]$ , is twice continuously differentiable at every point of $[0,1]$ , has $r(1)>0$ , and, for every $0<z<1$ , has $r(z)>0$ and satisfies

\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}.

Moreover, $D_r$ is interval integrable with respect to Lebesgue measure from $s$ to $1$ for every real $0<s<1$ . For every real $a$ with $0<a<1$ , the function $H$ is interval integrable with respect to Lebesgue measure from $a$ to $1$ , and there exist real constants $B>0$ and $M\ge\rho_{\min}$ such that, for every real $\rho\ge M$ ,

\left| K\int_a^1 D_{C(\rho)}(z)\,dz - K\left( \rho^2\int_a^1\frac{1}{z^3}\,dz+\int_a^1H(z)\,dz \right) \right| \le \frac{B}{\rho}.

The family $C$ and the threshold $\rho_{\min}$ are chosen before $a$ ; the constants $B$ and $M$ may depend on $a$ . No condition is imposed on $C(\rho)$ for $\rho<\rho_{\min}$ . All displayed quotients are real division, which assigns value zero when the denominator is zero.

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