[proofplan] We prove the Hopf Bifurcation Theorem by reducing the system to Poincare normal form and analysing the resulting amplitude equation. First, we use continuous dependence of eigenvalues to track the complex-conjugate pair $\lambda(\mu) = \alpha(\mu) \pm i\omega(\mu)$ across the bifurcation value $\mu = 0$. Second, we transform the planar system to polar-like coordinates via the Poincare normal form, which absorbs the angular dynamics into a rotation and isolates the radial dynamics as $\dot{r} = r(\alpha(\mu) - a r^2) + O(r^5)$. Third, we analyse the radial equation to locate the periodic orbit as a non-trivial zero of $\dot{r}$, compute its amplitude and period, and determine its stability from the sign of the first Lyapunov coefficient $a$. Finally, we establish uniqueness of the bifurcating periodic orbit near the origin. [/proofplan]

[step:Track the eigenvalues across the bifurcation and verify the crossing condition]The Jacobian $A(\mu) := Jf_{\mathbf{0}}(\mu) \in \mathbb{R}^{2 \times 2}$ depends smoothly on $\mu$ (since $\mathbf{f}$ is $C^k$ with $k \geq 4$). At $\mu = 0$, the eigenvalues are $\lambda(0) = \pm i\omega_0$ with $\omega_0 > 0$. Since $A(\mu)$ is a real $2 \times 2$ matrix with complex eigenvalues $\lambda(\mu) = \alpha(\mu) + i\omega(\mu)$ and $\overline{\lambda(\mu)} = \alpha(\mu) - i\omega(\mu)$, we have \begin{align*} \operatorname{tr} A(\mu) &= 2\alpha(\mu), \\ \det A(\mu) &= \alpha(\mu)^2 + \omega(\mu)^2. \end{align*} Both trace and determinant are smooth functions of $\mu$. At $\mu = 0$: $\alpha(0) = 0$ and $\omega(0) = \omega_0 > 0$. The transversality condition \begin{align*} \left.\frac{d\alpha}{d\mu}\right|_{\mu=0} = \frac{1}{2}\left.\frac{d}{d\mu}\operatorname{tr} A(\mu)\right|_{\mu=0} \neq 0 \end{align*} guarantees that the eigenvalues cross the imaginary axis with non-zero speed. By the implicit function theorem applied to $\alpha(\mu) = 0$, the crossing occurs at an isolated value of $\mu$, which we have normalised to $\mu = 0$. WLOG, assume $d\alpha/d\mu|_{\mu=0} > 0$ (the case $< 0$ is obtained by replacing $\mu$ with $-\mu$), so that \begin{align*} \alpha(\mu) < 0 \;\text{ for } \mu < 0, \qquad \alpha(0) = 0, \qquad \alpha(\mu) > 0 \;\text{ for } \mu > 0, \end{align*} in a neighbourhood of $\mu = 0$. The fixed point $\mathbf{0}$ is a stable focus for $\mu < 0$ and an unstable focus for $\mu > 0$.[/step]

[guided]The Jacobian $A(\mu) = Jf_{\mathbf{0}}(\mu)$ depends smoothly on the parameter $\mu$. Since $A(\mu)$ is a real $2 \times 2$ matrix, its eigenvalues come in complex-conjugate pairs: $\lambda(\mu) = \alpha(\mu) + i\omega(\mu)$ and $\overline{\lambda(\mu)} = \alpha(\mu) - i\omega(\mu)$. At $\mu = 0$, we are given $\lambda(0) = \pm i\omega_0$ with $\omega_0 > 0$, so $\alpha(0) = 0$ and $\omega(0) = \omega_0$. The trace and determinant formulas provide direct access to $\alpha$ and $\omega$: \begin{align*} \operatorname{tr} A(\mu) = 2\alpha(\mu), \qquad \det A(\mu) = \alpha(\mu)^2 + \omega(\mu)^2. \end{align*} Both are smooth functions of $\mu$. The transversality condition requires \begin{align*} \left.\frac{d\alpha}{d\mu}\right|_{\mu=0} = \frac{1}{2}\left.\frac{d}{d\mu}\operatorname{tr} A(\mu)\right|_{\mu=0} \neq 0. \end{align*} Why is transversality necessary? Without it, the eigenvalues could touch the imaginary axis and bounce back without crossing (as in $\alpha(\mu) = \mu^2$, which is non-negative for all $\mu$). The transversality condition ensures a genuine, transverse crossing: by the implicit function theorem applied to $\alpha(\mu) = 0$, the crossing occurs at an isolated value of $\mu$, which we normalise to $\mu = 0$. WLOG, assume $d\alpha/d\mu|_{\mu=0} > 0$ (the case $< 0$ is obtained by reparametrising $\mu \mapsto -\mu$). Then $\alpha(\mu) < 0$ for $\mu < 0$ (eigenvalues in the left half-plane, origin is a stable focus) and $\alpha(\mu) > 0$ for $\mu > 0$ (eigenvalues in the right half-plane, origin is an unstable focus). The stability of the fixed point switches at $\mu = 0$, and the question becomes: what replaces the stability that the origin has lost?[/guided]

[step:Transform to Poincare normal form and derive the amplitude equation]Near $\mu = 0$, apply a smooth $\mu$-dependent linear change of coordinates to put $A(\mu)$ in the standard form \begin{align*} A(\mu) = \begin{pmatrix} \alpha(\mu) & -\omega(\mu) \\ \omega(\mu) & \alpha(\mu) \end{pmatrix}, \end{align*} so the system becomes $\dot{\mathbf{x}} = A(\mu)\mathbf{x} + \mathbf{F}(\mathbf{x}; \mu)$, where $\mathbf{F}$ collects nonlinear terms of order $\geq 2$. Passing to polar coordinates $x_1 = r\cos\theta$, $x_2 = r\sin\theta$ (which is a smooth change of coordinates away from $r = 0$), the system takes the form \begin{align*} \dot{r} &= \alpha(\mu)\, r + \sum_{k=1}^{\infty} a_k(\mu)\, r^{2k+1} + \cdots, \\ \dot{\theta} &= \omega(\mu) + \sum_{k=1}^{\infty} b_k(\mu)\, r^{2k} + \cdots, \end{align*} where the coefficients $a_k(\mu)$, $b_k(\mu)$ are determined by the Taylor expansion of $\mathbf{F}$. The odd powers of $r$ in $\dot{r}$ and even powers in $\dot{\theta}$ arise from the rotational structure of the linear part: terms that break the $S^1$ symmetry of the linear part can be removed by a sequence of near-identity polynomial coordinate changes (the **Poincare normal form procedure**). More precisely, for each integer $m \geq 2$, one constructs a near-identity polynomial change of coordinates of degree $m$ that eliminates all non-resonant monomials of degree $\leq m$ in $\mathbf{F}$. Since the linear part has eigenvalues $\alpha \pm i\omega$ with $\omega \neq 0$, the resonant monomials (those that cannot be removed) are precisely those of the form $r^{2k+1}$ in $\dot{r}$ and $r^{2k}$ in $\dot{\theta}$. After normalisation up to order $3$, the system becomes \begin{align*} \dot{r} &= r\bigl(\alpha(\mu) - a\, r^2\bigr) + O(r^5), \\ \dot{\theta} &= \omega(\mu) + b\, r^2 + O(r^4), \end{align*} where $a = -a_1(0)$ is the **first Lyapunov coefficient**, computed from the third-order partial derivatives of $\mathbf{f}$ at $(\mathbf{0}; 0)$. The non-degeneracy condition requires $a \neq 0$.[/step]

[guided]The Poincare normal form is the central technical tool. The idea is to simplify the nonlinear terms of the ODE as much as possible by near-identity polynomial coordinate changes, while preserving the structure of the linear part. Near $\mu = 0$, a smooth $\mu$-dependent linear change of coordinates puts $A(\mu)$ in the standard form $\begin{pmatrix} \alpha(\mu) & -\omega(\mu) \\ \omega(\mu) & \alpha(\mu) \end{pmatrix}$. In polar coordinates $x_1 = r\cos\theta$, $x_2 = r\sin\theta$, the linear part becomes $\dot{r} = \alpha r$ and $\dot{\theta} = \omega$: pure radial growth/decay and pure rotation. The nonlinear terms $\mathbf{F}(\mathbf{x}; \mu)$ introduce coupling between $r$ and $\theta$, as well as angular dependence in both $\dot{r}$ and $\dot{\theta}$. The normal form procedure systematically removes the $\theta$-dependence, order by order. For each degree $m \geq 2$, one constructs a near-identity polynomial change of coordinates that eliminates all degree-$m$ monomials in $(r, \theta)$ that depend on $\theta$. This is achieved by solving the **homological equation**: for each monomial, one must divide by a factor involving the eigenvalues of $A$, which is non-zero precisely when the monomial is **non-resonant**. The non-resonance condition holds because $\omega_0 > 0$: the rotation in the linear part prevents any monomial involving $\theta$ from commuting with the flow. The resonant monomials -- those that cannot be removed -- are precisely the $\theta$-independent terms: $r^{2k+1}$ in $\dot{r}$ and $r^{2k}$ in $\dot{\theta}$. After normalising up to order $3$, the system becomes \begin{align*} \dot{r} &= r(\alpha(\mu) - a\,r^2) + O(r^5), \\ \dot{\theta} &= \omega(\mu) + b\,r^2 + O(r^4), \end{align*} where $a = -a_1(0)$ is the **first Lyapunov coefficient**. The coefficient $a$ is computed from the third-order partial derivatives of $\mathbf{f}$ at $(\mathbf{0}; 0)$; its explicit formula is lengthy, but what matters is that $a$ is determined by the $C^4$ jet of $\mathbf{f}$ (hence the hypothesis $k \geq 4$). The sign of $a$ determines the direction of branching. If $a > 0$, the cubic term $-ar^3$ opposes radial growth: for $\alpha > 0$, the radial equation has a stable non-trivial equilibrium at $r^* = \sqrt{\alpha/a}$, producing a stable limit cycle (supercritical bifurcation). If $a < 0$, the cubic term reinforces growth: for $\alpha < 0$, the non-trivial equilibrium is unstable, producing an unstable limit cycle (subcritical bifurcation). The non-degeneracy condition $a \neq 0$ excludes the degenerate case where the leading cubic balance vanishes and higher-order terms govern the bifurcation.[/guided]

[step:Analyse the radial equation to find the periodic orbit, its amplitude, and its period]Consider the truncated radial equation \begin{align*} \dot{r} = r\bigl(\alpha(\mu) - a\, r^2\bigr). \end{align*} The equilibria are $r = 0$ (the fixed point) and, when $\alpha(\mu)/a > 0$, \begin{align*} r^*(\mu) = \sqrt{\frac{\alpha(\mu)}{a}}. \end{align*} **Case $a > 0$ (supercritical).** Since $\alpha(\mu) > 0$ for $\mu > 0$ (by the transversality step), the non-trivial equilibrium $r^*(\mu) = \sqrt{\alpha(\mu)/a}$ exists for $\mu > 0$. To determine its stability, linearise $\dot{r} = r(\alpha - ar^2)$ about $r = r^*$: \begin{align*} \left.\frac{\partial}{\partial r}\bigl[r(\alpha - ar^2)\bigr]\right|_{r = r^*} = \alpha - 3a(r^*)^2 = \alpha - 3\alpha = -2\alpha(\mu) < 0. \end{align*} The negative sign confirms that $r^*$ is a stable equilibrium of the radial equation, so the corresponding circle $r = r^*(\mu)$ is a stable limit cycle of the planar system. Using $\alpha(\mu) = \alpha'(0)\mu + O(\mu^2)$ where $\alpha'(0) = d\alpha/d\mu|_{\mu=0} > 0$, the amplitude is \begin{align*} r^*(\mu) = \sqrt{\frac{\alpha'(0)\mu + O(\mu^2)}{a}} = \sqrt{\frac{\mu}{a}} \cdot \sqrt{\alpha'(0) + O(\mu)} = \sqrt{\frac{\mu}{a}}\bigl(1 + O(\mu)\bigr), \end{align*} after absorbing $\alpha'(0)$ into the parametrisation (which can be done by rescaling $\mu$, replacing $\mu$ with $\mu / \alpha'(0)$). The period is determined by the angular equation: \begin{align*} T(\mu) = \frac{2\pi}{\omega(\mu) + b\,(r^*)^2 + O((r^*)^4)} = \frac{2\pi}{\omega_0 + O(\mu)} = \frac{2\pi}{\omega_0} + O(\mu). \end{align*} For $\mu \leq 0$, the radial equation $\dot{r} = r(\alpha(\mu) - ar^2)$ with $\alpha(\mu) \leq 0$ has no positive equilibrium (since $\alpha/a \leq 0$), so $\dot{r} < 0$ for all $r > 0$: every trajectory spirals into the origin. No periodic orbit exists on this side. **Case $a < 0$ (subcritical).** The non-trivial equilibrium $r^* = \sqrt{\alpha(\mu)/a} = \sqrt{-\alpha(\mu)/|a|}$ exists for $\alpha(\mu) < 0$, i.e., $\mu < 0$. The linearisation at $r^*$ gives \begin{align*} \alpha - 3a(r^*)^2 = \alpha - 3\alpha = -2\alpha(\mu) > 0 \quad (\text{since } \alpha(\mu) < 0), \end{align*} so $r^*$ is an unstable equilibrium of the radial equation, producing an unstable limit cycle. The amplitude formula $r^*(\mu) = \sqrt{-\mu/|a|}(1 + O(\mu))$ and period formula $T(\mu) = 2\pi/\omega_0 + O(\mu)$ follow by the same argument. For $\mu \geq 0$, no positive equilibrium exists and no periodic orbit is present.[/step]

[guided]This step reduces the existence of a periodic orbit to elementary one-dimensional dynamics. Consider the truncated radial equation $\dot{r} = r(\alpha(\mu) - a\,r^2)$, which is a scalar ODE. Its equilibria are $r = 0$ and, when $\alpha(\mu)/a > 0$, the non-trivial value $r^*(\mu) = \sqrt{\alpha(\mu)/a}$. **Supercritical case ($a > 0$, $\mu > 0$).** Since $\alpha(\mu) > 0$ for $\mu > 0$, the non-trivial equilibrium $r^* = \sqrt{\alpha/a}$ exists. For small $r > 0$, the dominant term in $\dot{r}$ is $\alpha r > 0$: trajectories move radially outward. For large $r$, the cubic term $-ar^3$ dominates and $\dot{r} < 0$: trajectories move inward. The balance between these two forces occurs at $r = r^*$. Linearising: \begin{align*} \left.\frac{\partial}{\partial r}[r(\alpha - ar^2)]\right|_{r=r^*} = \alpha - 3a(r^*)^2 = \alpha - 3\alpha = -2\alpha(\mu) < 0, \end{align*} confirming that $r^*$ is a stable equilibrium of the radial equation. In the full two-dimensional system, the circle $r = r^*(\mu)$ is traversed at angular velocity $\dot{\theta} = \omega(\mu) + b(r^*)^2 + O((r^*)^4)$, giving a stable limit cycle. The amplitude and period are computed as follows. Using $\alpha(\mu) = \alpha'(0)\mu + O(\mu^2)$: \begin{align*} r^*(\mu) = \sqrt{\frac{\alpha(\mu)}{a}} = \sqrt{\frac{\mu}{a}}(1 + O(\mu)), \qquad T(\mu) = \frac{2\pi}{\omega(\mu) + O(\mu)} = \frac{2\pi}{\omega_0} + O(\mu). \end{align*} For $\mu \leq 0$, $\alpha(\mu) \leq 0$ gives $\alpha/a \leq 0$: no positive equilibrium exists, so $\dot{r} < 0$ for all $r > 0$ and every trajectory spirals into the origin. **Subcritical case ($a < 0$, $\mu < 0$).** Now $\alpha(\mu) < 0$ and $a < 0$, so $\alpha/a > 0$ and $r^* = \sqrt{\alpha/a} = \sqrt{|\alpha|/|a|}$ exists. The linearisation at $r^*$ gives $-2\alpha(\mu) > 0$ (since $\alpha < 0$), so $r^*$ is an unstable equilibrium. The corresponding limit cycle is unstable -- it separates trajectories converging to the origin from those escaping to larger radii. For $\mu \geq 0$, $\alpha(\mu) \geq 0$ with $a < 0$ gives $\alpha/a \leq 0$: no periodic orbit exists. The amplitude scaling $r^* \sim \sqrt{|\mu|}$ is characteristic of Hopf bifurcation and reflects the square-root balance between the linear growth rate $\alpha \sim \mu$ and the cubic saturation $ar^2$. This $\sqrt{|\mu|}$ law is the dynamical-systems analogue of the pitchfork bifurcation in one dimension. The period of the limit cycle is determined by the angular equation $\dot{\theta} = \omega(\mu) + b(r^*)^2 + O((r^*)^4)$. Since $r^* = O(\sqrt{|\mu|})$, the correction to the angular velocity is $O(|\mu|)$, and the period is \begin{align*} T(\mu) = \frac{2\pi}{\omega(\mu) + O(\mu)} = \frac{2\pi}{\omega_0 + O(\mu)} = \frac{2\pi}{\omega_0} + O(\mu). \end{align*} The leading-order period $2\pi/\omega_0$ is exactly the period of the linear oscillation at the bifurcation point $\mu = 0$. The limit cycle is born with the same period as the linearised oscillation, with $O(\mu)$ corrections from both the nonlinear frequency shift $b\,r^2$ and the variation $\omega(\mu) - \omega_0$.[/guided]

[step:Account for the higher-order remainder and establish uniqueness via the implicit function theorem]The full radial equation is $\dot{r} = r(\alpha(\mu) - a\,r^2) + R(r, \mu)$, where $R(r, \mu) = O(r^5)$ collects the remainder from the normal form truncation. Define \begin{align*} G: (0, \infty) \times \mathbb{R} &\to \mathbb{R}, \\ (r, \mu) &\mapsto \alpha(\mu) - a\,r^2 + r^{-1}R(r, \mu). \end{align*} A periodic orbit corresponds to a zero of $G$ at some $r > 0$. At the truncated solution $(r^*_0, \mu) = (\sqrt{\alpha(\mu)/a}, \mu)$, we have $G(r^*_0, \mu) = r_0^{*-1}R(r^*_0, \mu)$. Since $R = O(r^5)$, this is $O((r^*_0)^4) = O(\mu^2)$, which is a small perturbation. More precisely, define $\Phi(r, \mu) := \alpha(\mu) - a\,r^2 + r^{-1}R(r, \mu)$ for $r > 0$ near $0$ and $\mu$ near $0$. We compute \begin{align*} \Phi(0^+, 0) &= 0, \\ \frac{\partial \Phi}{\partial r}\bigg|_{(r^*, \mu)} &= -2a\,r^* + O((r^*)^3) \neq 0 \end{align*} for $r^*$ small and $a \neq 0$. By the implicit function theorem, there exists a unique smooth curve $r^*(\mu)$ near $(\mu, r) = (0, 0)$ with $\Phi(r^*(\mu), \mu) = 0$. The expansion \begin{align*} r^*(\mu) = \sqrt{\frac{\alpha(\mu)}{a}} + O(|\mu|^{3/2}) = \sqrt{\frac{\mu}{a}}\bigl(1 + O(\mu)\bigr) \end{align*} confirms the amplitude formula stated in the theorem. Uniqueness of the periodic orbit near the origin follows from uniqueness of the zero of $\Phi$: in a sufficiently small neighbourhood $U$ of $(\mathbf{0}, 0) \in \mathbb{R}^2 \times \mathbb{R}$, the implicit function theorem yields exactly one branch of zeros, hence exactly one periodic orbit for each $\mu$ on the appropriate side of the bifurcation. The stability conclusion carries over from the truncated system: the linearisation $\partial \Phi / \partial r|_{r = r^*(\mu)} = -2\alpha(\mu) + O(\mu^2)$ has the same sign as $-2\alpha(\mu)$ for $|\mu|$ small, confirming the stable (supercritical) or unstable (subcritical) character of $\Gamma_\mu$. This completes the proof of the Hopf Bifurcation Theorem.[/step]

[guided]The purpose of this final step is to justify that the higher-order remainder $R(r, \mu) = O(r^5)$ from the normal form truncation does not destroy the periodic orbit. The truncated equation $\dot{r} = r(\alpha - ar^2)$ has a zero at $r^* = \sqrt{\alpha/a}$, but the full equation is $\dot{r} = r(\alpha - ar^2) + R(r, \mu)$. Could the remainder shift this zero or eliminate it entirely? We address this by the implicit function theorem. Define $\Phi(r, \mu) := \alpha(\mu) - ar^2 + r^{-1}R(r, \mu)$ for $r > 0$ (dividing $\dot{r}$ by $r > 0$ is valid away from the origin). A periodic orbit corresponds to a zero $\Phi(r, \mu) = 0$ at some $r > 0$. At the truncated solution $(r^*_0, \mu) = (\sqrt{\alpha/a}, \mu)$, we have $\Phi(r^*_0, \mu) = r_0^{*-1}R(r^*_0, \mu) = O((r^*_0)^4) = O(\mu^2)$ -- a small perturbation of $0$. The key non-degeneracy condition is: \begin{align*} \frac{\partial \Phi}{\partial r}\bigg|_{(r^*, \mu)} = -2ar^* + O((r^*)^3) \neq 0 \end{align*} for $r^*$ small and $a \neq 0$. This is precisely where the non-degeneracy hypothesis $a \neq 0$ is consumed: it guarantees that the zero of $\Phi$ is a **simple root** with non-vanishing derivative, robust under small perturbations. The implicit function theorem then provides a unique smooth curve $r^*(\mu)$ near $(\mu, r) = (0, 0)$ with $\Phi(r^*(\mu), \mu) = 0$. The expansion $r^*(\mu) = \sqrt{\alpha(\mu)/a} + O(|\mu|^{3/2})$ confirms the amplitude formula. This curve represents the unique periodic orbit near the origin for each $\mu$ on the appropriate side of the bifurcation. **Stability.** The stability of the periodic orbit is determined by $\partial \Phi / \partial r|_{r = r^*(\mu)}$. Since $\partial \Phi / \partial r = -2\alpha(\mu) + O(\mu^2)$ and $\alpha(\mu)$ has definite sign for $\mu \neq 0$, the sign of $\partial \Phi / \partial r$ matches $-2\alpha(\mu)$ for small $|\mu|$. Negative means the zero is attracting (stable limit cycle, supercritical), positive means repelling (unstable limit cycle, subcritical). **Uniqueness.** No other periodic orbit exists in a small neighbourhood $U$ of $(\mathbf{0}, 0)$. Any additional zero of $\Phi$ in $U$ would violate the local uniqueness guarantee of the implicit function theorem, since $\partial \Phi / \partial r \neq 0$ throughout the region where $r$ and $|\mu|$ are small. This completes the proof of the Hopf Bifurcation Theorem.[/guided]