Nontrivial annular-boundary stationary surfaces

Open

QAlgorithms.Papers.Independent.Intakethird100.P58.appendix_annuli

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

prove2quantum

For each of the conformal and compactified D3 reduced models, there exist radii $0<R_i<R_e$ and a continuous direct profile $z:[R_i,R_e]\to\mathbb R$ , twice differentiable in the interior, such that

z(R_i)=z(R_e)=0,\qquad z(t)>0\quad(R_i<t<R_e).

In the compactified model $z(t)<1$ in the interior. The profile satisfies the Euler–Lagrange equation of $\int t z^{-3}\sqrt{B(z)+z'(t)^2}\,dt$ , where $B(z)=1$ in the conformal model and $B(z)=1-z^4$ in the compactified model. Rotating this graph gives a stationary surface ending on two distinct concentric boundary circles.

The radii are existential rather than arbitrary prescribed inputs. The result asserts stationarity and nontrivial annular boundary topology, and does not assert global minimality or turn the conjectural green-curve interpretation into a universal statement.

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.8--9,11,22--25: nontrivial annular-boundary stationary surfaces exist
in the conformal and compactified D3 reduced models. The radii are existential,
not arbitrary prescribed radii. No trajectory is declared globally minimizing. -/
theorem appendix_annuli :
    ∀ m : RotationalModel, (m = .conformal ∨ m = .d3) →
      ∃ (Ri Re : ℝ) (Z : ℝ → ℝ), IsAnnulus m Ri Re Z := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P58

end

Source

Topological Entanglement Entropy and Holography, arXiv:0805.1891v2, PDF p. 11, §3.2 and Appendix A, pp.22–25

Read-back

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

For every model $m$ among the three choices $\mathrm{conformal}$ , $\mathrm{d3}$ , and $\mathrm{d4}$ , if $m=\mathrm{conformal}$ or $m=\mathrm{d3}$ , there exist real numbers $R_i,R_e$ and a function $Z:\mathbb R\to\mathbb R$ such that $0<R_i<R_e$ , $Z$ is continuous on $[R_i,R_e]$ , and $Z(R_i)=Z(R_e)=0$ . At every $t\in(R_i,R_e)$ , the function $Z$ is twice continuously differentiable at $t$ , $Z(t)>0$ , and either $m=\mathrm{conformal}$ or $Z(t)<1$ . Define $w(s)=1$ and $v(s)=0$ when $m=\mathrm{conformal}$ , and $w(s)=1-s^4$ and $v(s)=-4s^3$ when $m=\mathrm{d3}$ . At every such interior point $t$ , the function satisfies

\left.\frac{d}{du} \left(\frac{uZ'(u)} {Z(u)^3\sqrt{w(Z(u))+(Z'(u))^2}}\right)\right|_{u=t} = t\left[ \frac{v(Z(t))} {2Z(t)^3\sqrt{w(Z(t))+(Z'(t))^2}} -\frac{3\sqrt{w(Z(t))+(Z'(t))^2}}{Z(t)^4} \right].

Thus the interior upper bound $Z(t)<1$ is required for the $\mathrm{d3}$ choice and is not required for the conformal choice. The premise is false for the $\mathrm{d4}$ choice, so that choice carries no existence conclusion.

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