Levi-Civita model and disk-like global sections

Phase. Phase is the type of all functions $s:\{0,1,2,3\}\to\mathbb R$, equivalently all ordered quadruples $s=(s_0,s_1,s_2,s_3)\in\mathbb R^4$, with no restrictions on their coordinates.

Plane. Plane is the type of all functions $u:\{0,1\}\to\mathbb R$, equivalently all ordered pairs $u=(u_0,u_1)\in\mathbb R^2$, with no restrictions on their coordinates.

qNormSq. For every phase point $s=(s_0,s_1,s_2,s_3)\in\mathbb R^4$, qNormSq is the real number $s_0^2+s_1^2$; it ignores $s_2$ and $s_3$ and is always nonnegative.

zNormSq. For every phase point $s=(s_0,s_1,s_2,s_3)\in\mathbb R^4$, zNormSq is the real number $s_0^2+s_1^2$; it is definitionally the same coordinate expression as qNormSq, ignores $s_2,s_3$, and is always nonnegative.

wNormSq. For every phase point $s=(s_0,s_1,s_2,s_3)\in\mathbb R^4$, wNormSq is the real number $s_2^2+s_3^2$; it ignores $s_0,s_1$ and is always nonnegative.

jacobiHamiltonian. For every $\mu\in\mathbb R$ and $s=(s_0,s_1,s_2,s_3)\in\mathbb R^4$, jacobiHamiltonian is the total real-valued function

$$H_\mu(s)=\frac{s_2^2+s_3^2}{2}+s_0s_3-s_1s_2-\frac{1-\mu}{\sqrt{(s_0+\mu)^2+s_1^2}}-\frac{\mu}{\sqrt{(s_0-1+\mu)^2+s_1^2}}.$$

There is no assumption on $\mu$ or exclusion of collision points. The square roots are the nonnegative real square roots, and real division is totalized: whenever either square-root denominator is $0$, its corresponding quotient is defined to be $0$, rather than being undefined or infinite.

collisionFree. For every $\mu\in\mathbb R$ and phase point $s$, collisionFree μ s means precisely

$$0<(s_0+\mu)^2+s_1^2 \quad\text{and}\quad 0<(s_0-1+\mu)^2+s_1^2.$$

Thus both displayed squared distances must be strictly positive; no restriction such as $0<\mu<1$ is included.

coordinateVector. For each index $i\in\{0,1,2,3\}$, coordinateVector i is the phase vector $e_i\in\mathbb R^4$ whose $j$-th coordinate is $1$ when $j=i$ and $0$ otherwise.

partialDerivative. For every function $F:\mathbb R^4\to\mathbb R$, phase point $s$, and coordinate index $i\in\{0,1,2,3\}$, partialDerivative F s i is $D^{\mathrm{tot}}F(s)[e_i]$, the totalized Fréchet derivative of $F$ at $s$ applied to the $i$-th coordinate vector. When $F$ is Fréchet differentiable at $s$, this is its $i$-th coordinate derivative; when no Fréchet derivative exists, Lean’s totalized fderiv is the zero linear map, so the defined value is $0$.

hamiltonianVectorField. For every $F:\mathbb R^4\to\mathbb R$ and $s\in\mathbb R^4$, hamiltonianVectorField F s is

$$\bigl(D^{\mathrm{tot}}F(s)[e_2],\ D^{\mathrm{tot}}F(s)[e_3],\ -D^{\mathrm{tot}}F(s)[e_0],\ -D^{\mathrm{tot}}F(s)[e_1]\bigr).$$

All four entries use the totalized Fréchet derivative, so a failure of differentiability makes that derivative the zero linear map rather than making the vector field undefined.

isCriticalPoint. For every $F:\mathbb R^4\to\mathbb R$ and $s\in\mathbb R^4$, isCriticalPoint F s means $D^{\mathrm{tot}}F(s)=0$ as a continuous linear functional on $\mathbb R^4$. Because fderiv is totalized to the zero map at a point where no Fréchet derivative exists, such a nondifferentiability point also satisfies this predicate.

firstCriticalValue. For every $\mu\in\mathbb R$, firstCriticalValue μ is

$$\inf\left\{e\in\mathbb R\ \middle|\ \begin{array}{l} \text{there exists }s\in\mathbb R^4\text{ with }(s_0+\mu)^2+s_1^2>0,\\ (s_0-1+\mu)^2+s_1^2>0,\quad D^{\mathrm{tot}}H_\mu(s)=0,\quad H_\mu(s)=e \end{array}\right\},$$

where $H_\mu$ is the formula in jacobiHamiltonian, including its totalized divisions. This is an infimum, not an assertion that a smallest value is attained. No hypothesis says that the set is nonempty or bounded below; sInf nevertheless remains a total real-valued operation in those degenerate cases, without the usual mathematical characterization of an infimum being guaranteed.

belowFirstCriticalValue. For every $\mu,c\in\mathbb R$, belowFirstCriticalValue μ c is exactly the strict inequality

$$-c<\operatorname{sInf}\{H_\mu(s)\mid s\text{ is collision-free and }D^{\mathrm{tot}}H_\mu(s)=0\}.$$

It adds no assumptions on $\mu,c$, on existence of collision-free critical points, or on attainment of the infimum.

secondCollisionDistanceSq. For every phase point $s$, secondCollisionDistanceSq s is

$$D(s)=\bigl(2(s_0^2-s_1^2)-1\bigr)^2+(4s_0s_1)^2.$$

It depends only on $s_0,s_1$, is always nonnegative, and is $0$ exactly when $s_1=0$ and $s_0^2=\tfrac12$, with $s_2,s_3$ arbitrary.

leviCivitaHamiltonian. For every $\mu,c\in\mathbb R$ and $s\in\mathbb R^4$, leviCivitaHamiltonian μ c s is the total real number

$$K_{\mu,c}(s)=\frac{s_2^2+s_3^2}{2}+c(s_0^2+s_1^2)-\frac{1-\mu}{2} +2(s_0^2+s_1^2)(s_0s_3-s_1s_2)-\mu(s_0s_3+s_1s_2) -\frac{\mu(s_0^2+s_1^2)}{\sqrt{D(s)}},$$

where $D(s)=\bigl(2(s_0^2-s_1^2)-1\bigr)^2+(4s_0s_1)^2$. There are no restrictions on $\mu,c,s$. At $D(s)=0$, the final quotient is defined to be $0$ by totalized real division.

leftCollisionPoint. For every $\mu\in\mathbb R$, leftCollisionPoint μ is the phase point

$$a_\mu=(0,0,\sqrt{1-\mu},0).$$

The square root is the nonnegative real square root; in particular, if $\mu>1$, then $\sqrt{1-\mu}=0$, so $a_\mu=(0,0,0,0)$.

regularEnergyLocus. For every $\mu,c\in\mathbb R$, regularEnergyLocus μ c is the set of all $s\in\mathbb R^4$ satisfying

$$K_{\mu,c}(s)=0 \quad\text{and}\quad D(s)>0,$$

where

$$D(s)=\bigl(2(s_0^2-s_1^2)-1\bigr)^2+(4s_0s_1)^2$$

and

$$K_{\mu,c}(s)=\frac{s_2^2+s_3^2}{2}+c(s_0^2+s_1^2)-\frac{1-\mu}{2} +2(s_0^2+s_1^2)(s_0s_3-s_1s_2)-\mu(s_0s_3+s_1s_2) -\frac{\mu(s_0^2+s_1^2)}{\sqrt{D(s)}}.$$

The strict inequality excludes every zero of the square-root denominator.

leftEnergyComponent. For every $\mu,c\in\mathbb R$, leftEnergyComponent μ c is the connected component, within the set $\{s\in\mathbb R^4\mid K_{\mu,c}(s)=0\ \text{and}\ D(s)>0\}$, based at $a_\mu=(0,0,\sqrt{1-\mu},0)$, where

$$D(s)=\bigl(2(s_0^2-s_1^2)-1\bigr)^2+(4s_0s_1)^2$$

and

$$K_{\mu,c}(s)=\frac{s_2^2+s_3^2}{2}+c(s_0^2+s_1^2)-\frac{1-\mu}{2} +2(s_0^2+s_1^2)(s_0s_3-s_1s_2)-\mu(s_0s_3+s_1s_2) -\frac{\mu(s_0^2+s_1^2)}{\sqrt{D(s)}}.$$

No hypothesis ensures that the base point belongs to this set; if it does not, the connected component in the set is empty. In particular, for $\mu>1$, $a_\mu=(0,0,0,0)$ and $K_{\mu,c}(a_\mu)=(\mu-1)/2>0$, so this component is empty.

LeftEnergyState. For every $\mu,c\in\mathbb R$, LeftEnergyState μ c is the subtype consisting of phase points $s\in\mathbb R^4$ that lie in the connected component, based at $(0,0,\sqrt{1-\mu},0)$, of the set on which $K_{\mu,c}(s)=0$ and $D(s)>0$, with $D$ and $K_{\mu,c}$ given by

$$D(s)=\bigl(2(s_0^2-s_1^2)-1\bigr)^2+(4s_0s_1)^2,\qquad K_{\mu,c}(s)=\frac{s_2^2+s_3^2}{2}+c(s_0^2+s_1^2)-\frac{1-\mu}{2}+2(s_0^2+s_1^2)(s_0s_3-s_1s_2)-\mu(s_0s_3+s_1s_2)-\frac{\mu(s_0^2+s_1^2)}{\sqrt{D(s)}}.$$

An inhabitant carries both a phase point and proof of membership; the type may be empty, in particular when $\mu>1$.

IsLeviCivitaHamiltonianFlow. For every $\mu,c\in\mathbb R$ and every continuous real flow $\phi$ on the subtype $E_{\mu,c}$ of phase points in the connected component, based at $(0,0,\sqrt{1-\mu},0)$, of $\{K_{\mu,c}=0,\ D>0\}$, IsLeviCivitaHamiltonianFlow μ c φ means that for every $s\in E_{\mu,c}$, the phase-space curve $t\mapsto\phi_t(s)$ is differentiable at $t=0$ with

$$\left.\frac{d}{dt}\right|_{t=0}\phi_t(s) =\bigl(DK_{\mu,c}(s)[e_2],DK_{\mu,c}(s)[e_3],-DK_{\mu,c}(s)[e_0],-DK_{\mu,c}(s)[e_1]\bigr),$$

where $D(x)=\bigl(2(x_0^2-x_1^2)-1\bigr)^2+(4x_0x_1)^2$ and

$$K_{\mu,c}(x)=\frac{x_2^2+x_3^2}{2}+c(x_0^2+x_1^2)-\frac{1-\mu}{2}+2(x_0^2+x_1^2)(x_0x_3-x_1x_2)-\mu(x_0x_3+x_1x_2)-\frac{\mu(x_0^2+x_1^2)}{\sqrt{D(x)}}.$$

The right-hand derivatives are totalized Fréchet derivatives. The declaration directly requires the trajectory derivative only at time $0$, separately for every state; if $E_{\mu,c}$ is empty, the universal condition is vacuous.

PeriodicOrbit. For every type $X$ equipped with a topological-space structure and every real flow $\phi$ on $X$, PeriodicOrbit φ is a structure containing a point $x\in X$, a real number $T$, a proof that $T>0$, and a proof that $\phi_T(x)=x$. It does not require $T$ to be the least positive return time, does not require the trajectory to be nonconstant, and therefore permits a fixed point whenever it is returned to itself after a chosen positive time.

orbitSet. For every $\mu,c\in\mathbb R$, every continuous real flow $\phi$ on the subtype $E_{\mu,c}$ consisting of the connected component of $\{K_{\mu,c}=0,\ D>0\}$ based at $(0,0,\sqrt{1-\mu},0)$, and every periodic-orbit record $\gamma$ for $\phi$ with point $x_\gamma$, positive period $T_\gamma$, and $\phi_{T_\gamma}(x_\gamma)=x_\gamma$, orbitSet γ is

$$\{\phi_t(x_\gamma)\in\mathbb R^4\mid t\in\mathbb R\},$$

where subtype values are forgotten and viewed as phase points. Here $D(s)=\bigl(2(s_0^2-s_1^2)-1\bigr)^2+(4s_0s_1)^2$, and $K_{\mu,c}$ is the displayed Levi–Civita formula. The set uses only $\gamma$’s point and the flow; the recorded period itself does not appear in its definition.

planeNormSq. For every $u=(u_0,u_1)\in\mathbb R^2$, planeNormSq u is $u_0^2+u_1^2$, which is always nonnegative.

closedUnitDisk. closedUnitDisk is the set

$$\{u=(u_0,u_1)\in\mathbb R^2\mid u_0^2+u_1^2\le 1\}.$$

openUnitDisk. openUnitDisk is the set

$$\{u=(u_0,u_1)\in\mathbb R^2\mid u_0^2+u_1^2<1\}.$$

unitCircle. unitCircle is the set

$$\{u=(u_0,u_1)\in\mathbb R^2\mid u_0^2+u_1^2=1\}.$$

DiskLikeGlobalSurfaceOfSection. For every $\mu,c\in\mathbb R$, every continuous real flow $\phi$ on $E_{\mu,c}$, and every periodic-orbit record $\gamma$ for $\phi$, DiskLikeGlobalSurfaceOfSection φ γ means that there exists a globally defined map $p:\mathbb R^2\to\mathbb R^4$ such that, writing $B=\{u\mid u_0^2+u_1^2\le1\}$, $B^\circ=\{u\mid u_0^2+u_1^2<1\}$, $C=\{u\mid u_0^2+u_1^2=1\}$, and $E_{\mu,c}$ for the connected component based at $(0,0,\sqrt{1-\mu},0)$ of $\{s\mid K_{\mu,c}(s)=0,\ D(s)>0\}$: $p$ is $C^\infty$ on $B$ in the relative ContDiffOn sense; $p(u)\in E_{\mu,c}$ for every $u\in B$; $p$ is injective on $B$; for every $u\in B$, the totalized full Fréchet derivative $Dp(u):\mathbb R^2\to\mathbb R^4$ is injective; $p(C)=\{\phi_t(\gamma.\mathrm{point})\mid t\in\mathbb R\}$ as sets; for every $s\in E_{\mu,c}$ whose phase point lies in $p(B^\circ)$, there exists $\varepsilon>0$ such that for every $t\in\mathbb R$, if $|t|<\varepsilon$ and $\phi_t(s)\in p(B^\circ)$, then $t=0$; and for every $s\in E_{\mu,c}$ not lying on $\{\phi_t(\gamma.\mathrm{point})\mid t\in\mathbb R\}$, there exist separately a time $t_+>0$ and a time $t_-<0$ with $\phi_{t_+}(s),\phi_{t_-}(s)\in p(B^\circ)$. Here

$$D(s)=\bigl(2(s_0^2-s_1^2)-1\bigr)^2+(4s_0s_1)^2$$

and

$$K_{\mu,c}(s)=\frac{s_2^2+s_3^2}{2}+c(s_0^2+s_1^2)-\frac{1-\mu}{2}+2(s_0^2+s_1^2)(s_0s_3-s_1s_2)-\mu(s_0s_3+s_1s_2)-\frac{\mu(s_0^2+s_1^2)}{\sqrt{D(s)}}.$$

The condition imposes no positive- or negative-time interior intersection requirement on states belonging to $\gamma$’s orbit, does not require first or unique return times, and does not otherwise use $\gamma$’s recorded period.

IsStrictlyConvexLevel. For every arbitrary function $F:\mathbb R^4\to\mathbb R$ and arbitrary set $S\subseteq\mathbb R^4$, IsStrictlyConvexLevel F S means that for every $s\in S$ and every nonzero $v\in\mathbb R^4$, if $D^{\mathrm{tot}}F(s)[v]=0$, then

$$D^{\mathrm{tot}}\!\left(x\mapsto D^{\mathrm{tot}}F(x)[v]\right)(s)[v]>0.$$

Both derivatives are Lean’s totalized Fréchet derivatives. No differentiability or twice-differentiability hypothesis on $F$ is stated, and $S$ is not required to be a level set, a hypersurface, nonempty, or regular; in particular, the proposition is vacuously true when $S=\varnothing$.