A certified interval Hopf record verifies only the local Hopf hypotheses

By [F1], the root field has either an exact zero or a root-isolation record satisfying the hypotheses of [F2]; in the latter case [F2] proves the unique represented equilibrium exists in the specified ball.

By [F1], the accepted Jacobian and derivative data are proved to be those of the exact represented equilibrium (or the unique isolated branch), and the eigenpair and multiplicity-cover witnesses enclose its exact spectrum. Their strict conditions give a simple conjugate pair with positive frequency and put every other eigenvalue strictly off the imaginary axis. Write the represented exact point as $(x_{\ast },{\lambda }_0)$ and translate by $\widehat{f}(y,\mu )=f(x_{\ast }+y,{\lambda }_0+\mu )$. Its origin jets are precisely the accepted $A,B,C$, its critical eigenpair is the accepted normalized pair, and its equilibrium-branch derivative is the accepted derivative with respect to $\mu$. This identifies the record with the base-point convention of Hopf spectral and multilinear normal-form data and the equilibrium $(x_{\ast },0)$ after parameter translation in [F3].

The exact values ${\beta }^{\mathrm{\prime }}$ and ${\mathrm{\ell }}_1$ lie in their certified intervals by the input-witness condition. Since the algorithm accepts only intervals disjoint from zero, both exact values are nonzero. The eigenvalue branch derivative is the one in A simple eigenpair has a regularity-matched gauge-fixed parameter branch, and the coefficient is the normalization in Hopf spectral and multilinear normal-form data.

Steps 1.1–2.1 establish every hypothesis of [F3]. Applying [F3] gives the local branch, its parameter side, and the stated local Floquet classification. None of these local hypotheses or conclusions asserts a global orbit or a global continuation trace, so the certificate carries no such implication.