1: \begin{proof}

2:  The validation is split into three steps.

3:  \begin{enumerate}

4:   \item From Theorem~\ref{thm:main_isochronous} we know, that there is an \isoname bifurcation of halo orbits from $L_2$-Lyapunov family. The estimates (\ref{eq:BoundOnDYAtMinimum}) are taken from this proof. The branching of family of halo orbits $h_\mu(z) = (x_\mu(z),0,z,0,\dot y_\mu(z),0)$ is parametrized by $z\in[-1,1]\cdot \Delta_z$, with $\Delta_z=10^{-7}$. We also check that $\dot y_\mu''(z)>0$ for $|z|\leq \Delta_z$.

5:   \item The branch is then rigorously continued using \ref{sec:continuation} and parametrized by $h_\mu(z) = (x_\mu(z),0,z,0,\dot y_\mu(z),0)$, $z>0$ until some hand-chosen threshold value of $\hat z$ (dependent on $\mu$). We also checked that for $z\in[\Delta z,\hat z]$ there holds $\dot y_\mu'(z)>0$.

6:   \item Further continuation of the branch starting from $h_\mu(\hat z)$ is parametrized by $\dot y$ until hand-chosen threshold values (\ref{eq:dytreshhold}). 

7:  \end{enumerate}

8: Summarizing, in each segment the variable $\dot y$ is increasing along the branch of periodic orbits which makes it possible to re-parametrize the curve as a function 

9: $$h_\mu(\tau)=(x_\mu(\tau),0,z_\mu(\tau),0,\dot y_\mu(\tau),0)$$

10: defined on $\tau\in[0,1]$. From the symmetry $S$ we obtain the second branch for $\tau\in[-1,0]$.

11: 

12: The bifurcations listed in Table~\ref{tab:L2Tuplings} (except $j=0$) were validated using Theorem~\ref{thm:Htupling} and Theorem~\ref{thm:Htag} in high-precision interval arithmetics. Notice, that in two cases $j=8$ and $\mu=\{\muSJ,\muEM\}$ we could not obtain bounds on third order derivatives sharp enough to check convexity of Jacobi integral along bifurcation curve. We checked, however, the conditions \textbf{HC2--HC4}, which in particular means, that there are two curves of halo orbits of period $1$ and $4$ intersecting at a single point.  

13: \end{proof}

14: