Reported shrinking oscillations of the D4 shooting families

Open

QAlgorithms.Papers.Independent.Intakethird100.P58.d4_branch_oscillations

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

prove2quantum

For the physical D4 reduced equation there exist regular disk profiles indexed by their axis depth $s\in(0,1)$ , with boundary radii $\rho_D(s)$ , and regular cylinder profiles indexed by their endpoint radii $t>0$ , with boundary radii $\rho_C(t)$ . The radius functions are continuous on their parameter intervals. The numerical study reported in the source finds a common finite $\rho_c>0$ with

\rho_D(s)\longrightarrow\rho_c\quad(s\to1^-),\qquad \rho_C(t)\longrightarrow\rho_c\quad(t\to0^+),

and both radius functions take values strictly above and strictly below $\rho_c$ in every punctured neighborhood of their limiting parameter.

Finite limiting radius together with these repeated crossings is the qualitative diminishing-envelope interpretation of the reported oscillations. No decay rate, exact critical decimal, or exhaustive count of solutions at a prescribed radius is asserted.

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.17--18: the reported numerical shrinking oscillations of the D4
shooting families. This records a qualitative numerical finding of the source,
not a certified rate or an assertion of exactly two solutions at a fixed radius. -/
theorem d4_branch_oscillations :
    ∃ (R : ℝ → ℝ) (D C : ℝ → ℝ → ℝ) (critical : ℝ),
      0 < critical ∧
      (∀ s ∈ Ioo (0 : ℝ) 1, IsDisk .d4 (R s) s (D s)) ∧
      (∀ t : ℝ, 0 < t → IsCylinder .d4 (C t 0) (C t) ∧ C t 1 = t) ∧
      ContinuousOn R (Ioo (0 : ℝ) 1) ∧
      ContinuousOn (fun t => C t 0) (Ioi (0 : ℝ)) ∧
      ShrinkingOscillations R (Ioo 0 1) 1 critical ∧
      ShrinkingOscillations (fun t => C t 0) (Ioi 0) 0 critical := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P58

end

Source

Topological Entanglement Entropy and Holography, arXiv:0805.1891v2, PDF p. 17, §4.1, Figs.8–9

Read-back

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

There exist functions $R:\mathbb R\to\mathbb R$ and $D,C:\mathbb R\to\mathbb R\to\mathbb R$ , and a real number $q>0$ , with the following properties. To specify their required profile conditions, say that a function $p:\mathbb R\to\mathbb R$ satisfies the regular conditions with parameters $A,b\in\mathbb R$ when $A>0$ , $b>0$ , $p(0)=A$ , $p$ is continuous and strictly decreasing on $[0,b]$ , $p$ is twice continuously differentiable at every point of $[0,b)$ as a function on $\mathbb R$ , and for every $z\in(0,b)$ ,

p(z)>0,\qquad \left.\frac{d}{du} \left( \frac{p(u)^2u(1-u^3)p'(u)} {u^3\sqrt{1+u(1-u^3)p'(u)^2}} \right)\right|_{u=z} = \frac{2p(z)}{z^3}\sqrt{1+z(1-z^3)p'(z)^2},

and, for every real $a$ with $0<a<b$ , the function $z\mapsto p(z)^2\sqrt{1+z(1-z^3)p'(z)^2}/z^3$ is Lebesgue interval-integrable from $a$ to $b$ . For every $s\in(0,1)$ , the function $d_s(z)=D(s,z)$ satisfies these regular conditions with $A=R(s)$ and $b=s$ , has $d_s(s)=0$ , and its function

H_s(v)=\inf\{z\in[0,s]:d_s(z)=v\},

assigned value $0$ when the set is empty, is twice continuously differentiable within $[0,R(s))$ and has derivative $0$ at $0$ within $[0,\infty)$ . For every real $t>0$ , the function $c_t(z)=C(t,z)$ satisfies the regular conditions with $A=C(t,0)$ and $b=1$ , has $c_t(1)=t>0$ , and is twice continuously differentiable at $1$ as a function on $\mathbb R$ . Furthermore, $R$ is continuous on $(0,1)$ , the function $t\mapsto C(t,0)$ is continuous on $(0,\infty)$ , and

\lim_{s\to1^-}R(s)=q, \qquad \lim_{t\to0^+}C(t,0)=q.

For every real $\delta>0$ , there are $s_-,s_+\in(0,1)$ and $t_-,t_+>0$ satisfying

\begin{gathered} 0<|s_--1|<\delta,\quad R(s_-)<q,\qquad 0<|s_+-1|<\delta,\quad q<R(s_+),\\ 0<t_-<\delta,\quad C(t_-,0)<q,\qquad 0<t_+<\delta,\quad q<C(t_+,0). \end{gathered}

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