Regular D4 large-ball coefficient hierarchy

Open

QAlgorithms.Papers.Independent.Intakethird100.P58.d4_profile_coefficient

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

prove2quantum

Consider the regular coefficient problems obtained by equating powers in the D4 large-radius ansatz $r(z)=\rho+f(z)+g(z)/\rho+\cdots$ . The leading problem is (4.19), with $f(0)=0$ and regularity at $z=1$ ; the next problem after that leading coefficient vanishes is

4+(4+2z^3)g'(z)-2z(1-z^3)g''(z)=0,\qquad g(0)=0.

The leading regular coefficient exists and is $f=0$ . The next regular coefficient exists, is unique on $[0,1]$ , and is

g(z)=-\frac{\arctan((1+2z)/\sqrt3)}{\sqrt3}-\frac12\log(1+z+z^2)+\frac{\pi}{6\sqrt3},\qquad g'(z)=-\frac{1+z}{1+z+z^2}.

In the unsimplified interior expression $g'(z)=-(1+cz^2)/(1-z^3)$ , regularity forces $c=-1$ . In particular $g'(1)=-2/3$ , using the simplified formula. Locally at zero,

g(z)=-z+\frac{z^3}{3}-\frac{z^4}{4}+\frac{z^6}{6}-\frac{z^7}{7}+\frac{z^9}{9}+O(z^{10}).

This is the analytic coefficient result for the formal hierarchy, including uniqueness and regular endpoint data. It does not assume an asymptotic expansion of a free surface profile, or assert convergence at $z=1$ .

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.19)--(4.23): the regular coefficient hierarchy gives f=0
and the unique g on [0,1], with integration constant c=-1. The Taylor display
is only a finite local asymptotic statement, not a series equality at z=1. -/
theorem d4_profile_coefficient :
    (∃ f : ℝ → ℝ, FirstD4Coefficient f) ∧
    (∀ f : ℝ → ℝ, FirstD4Coefficient f → ∀ z ∈ Icc (0 : ℝ) 1, f z = 0) ∧
    (∃ g : ℝ → ℝ, SecondD4Coefficient g ∧
      (∀ z ∈ Icc (0 : ℝ) 1, g z = d4G z ∧ deriv g z = d4GPrime z) ∧
      (∀ c : ℝ, (∀ z ∈ Ioo (0 : ℝ) 1,
        deriv g z = -(1 + c * z ^ 2) / (1 - z ^ 3)) ↔ c = -1)) ∧
    (∀ g : ℝ → ℝ, SecondD4Coefficient g → ∀ z ∈ Icc (0 : ℝ) 1, g z = d4G z) ∧
    Asymptotics.IsBigO (nhds (0 : ℝ))
      (fun z => d4G z - (-z + z ^ 3 / 3 - z ^ 4 / 4 + z ^ 6 / 6 - z ^ 7 / 7 + z ^ 9 / 9))
      (fun z => z ^ 10) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P58

end

Source

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

Read-back

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

For a function $f:\mathbb R\to\mathbb R$ , let condition $A$ mean that $f(0)=0$ , that $f$ is twice continuously differentiable at every point of $[0,1]$ , including both endpoints, and that, for every $0<z<1$ ,

4f'(z)+2z^3f'(z)+5z(f'(z))^3-7z^4(f'(z))^3+2z^7(f'(z))^3-2zf''(z)+2z^4f''(z)=0.

For a function $g:\mathbb R\to\mathbb R$ , let condition $B$ mean that $g(0)=0$ , that $g$ is twice continuously differentiable at every point of $[0,1]$ , including both endpoints, and that, for every $0<z<1$ ,

4+4g'(z)+2z^3g'(z)-2zg''(z)+2z^4g''(z)=0.

Define, for real $z$ ,

G(z)=-\frac{\arctan((1+2z)/\sqrt3)}{\sqrt3} -\frac{\log(1+z+z^2)}2+\frac{\pi}{6\sqrt3}, \qquad Q(z)=-\frac{1+z}{1+z+z^2}.

The assertion is the conjunction of the following claims: there exists an $f$ satisfying $A$ ; every $f$ satisfying $A$ obeys $f(z)=0$ for all $z\in[0,1]$ ; there exists a $g$ satisfying $B$ such that $g(z)=G(z)$ and $g'(z)=Q(z)$ for every $z\in[0,1]$ , and such that, for every real $c$ ,

\left(\forall z\in(0,1),\quad g'(z)=-\frac{1+cz^2}{1-z^3}\right) \quad\Longleftrightarrow\quad c=-1;

every $g$ satisfying $B$ obeys $g(z)=G(z)$ for all $z\in[0,1]$ ; and, as $z\to0$ through real values from either side,

G(z)-\left(-z+\frac{z^3}{3}-\frac{z^4}{4}+\frac{z^6}{6}-\frac{z^7}{7}+\frac{z^9}{9}\right)=O(z^{10}).

The last claim means that there exist constants $K>0$ and $\delta>0$ such that the absolute value of the displayed difference is at most $K|z^{10}|$ whenever $|z|<\delta$ . The conclusions identifying $f$ and $g$ specify their values only on $[0,1]$ .

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