Linearisation gives eigenvalue $-2$. Gronwall gives a symmetric ball $|r-1|<1/3$. DOP853 says the real inner edge is $r_\star \approx 0.80$. The gap is the course.
Objective: prove exponential contraction and expose the asymmetry
|Pre-req: S1
|Mode: lecture + numerical demo
Theorem 2.1 · Helical Attractor, symmetric version
There exists $\varepsilon_0 > 0$ such that every solution with $|r(0) - 1| < \varepsilon_0$ satisfies
$$\limsup_{t\to\infty} \frac{1}{t}\,\log|r(t) - 1| \;\leq\; -2,$$
and consequently $r(t) \to 1$, $z(t)/t \to 1$, $\theta(t) - t \to \text{const}$; i.e. the trajectory converges to the helix $\Gamma = \{r = 1\}$ at rate exactly $e^{-2t}$. The elementary Gronwall argument gives $\varepsilon_0 = 1/3$. See §3 below.
Read the theorem closely: the rate $\mu = -2$ is sharp — it is the Jacobian eigenvalue, not a Lyapunov bound. The basin $\varepsilon_0$ is where the trouble lives. Every step below either improves or sharpens that constant.
§2 · Where $-2$ Comes From
Linearisation at $r = 1$
Set $u = r - 1$ and expand the radial equation. On $r = 1$ the coupling vanishes identically, so to first order the $\varepsilon$-term contributes nothing to the linear part. The Hopf term $r(1-r^2) = -2u + O(u^2)$. Hence
$\dot u \;=\; -2 u \;+\; O(u^2) \;+\; O(\varepsilon\, u\, e^{-z}).$
The linear-in-$u$ contribution from the coupling $\varepsilon(r-1)e^{-z} = \varepsilon\,u\,e^{-z}$ is explicit: it carries a factor of $e^{-z(t)}$. Since $\dot z \to 1$ along any nearby orbit, $z(t) \to +\infty$ and $e^{-z(t)} \to 0$. The coupling-linear piece is a decaying perturbation of the strict $-2$ rate.
Observation 2.2 · The eigenvalue is exact
Linearising the full system at any point $(\theta, z)$ of the limit cycle $\Gamma = \{r=1\}$ gives a block-triangular Jacobian whose radial eigenvalue is $\mu = \partial_r\,\dot r \big|_{r=1} = 1 - 3r^2 + \varepsilon\,e^{-z}\big|_{r=1} = -2 + \varepsilon\,e^{-z}$. As $z\to\infty$ the perturbation vanishes and the eigenvalue tends to $-2$. This is why every numerical trajectory in Table 1 will read out a $\hat\mu$ close to but slightly less negative than $-2$ — we are seeing $-2 + \varepsilon\,e^{-z}$ averaged over the transient.
So where does $-2$ come from in one line?
From $\tfrac{d}{dr}\bigl[r - r^3\bigr]_{r=1} = 1 - 3 = -2$. The Hopf normal form alone delivers the rate. The contact coupling does not alter it. Every other term in the system is either higher order in $u$ or suppressed by $e^{-z}$.
§3 · Where $1/3$ Comes From
The Gronwall Sketch
We want a non-linear, explicit basin — the set of initial $r(0)$ for which we can prove $r(t) \to 1$. The cleanest route is an energy-style Gronwall argument in $u = r - 1$.
Step 1. The scalar inequality.
Multiply the radial equation by $u$ and expand $r(1-r^2) = -2u - 3u^2 - u^3$. One obtains
The dangerous terms for small-$u$ analysis are $-3u^3$ (which can switch sign) and the $\varepsilon$ term (which is positive and only decays with $z$). We keep the rest as a clean $-2u^2 - u^4 \leq -2u^2$.
Step 2. Bound the bad pieces.
Assume $|u(0)| < \varepsilon_0$ and, as an induction hypothesis, $|u(t)| < \varepsilon_0$ for all $t$ considered. Then $|3u^3| \leq 3\varepsilon_0 u^2$. We also need $z(t) \geq z(0) - \delta$ for some bookkeeping $\delta$; a short argument using $\dot z = 1 + O(u^2)$ gives $\dot z \geq 1 - \varepsilon_0^2$, hence $e^{-z(t)} \leq e^{-z(0)}\,e^{(\varepsilon_0^2)\,t}$. For the exponent to stay useful we need $\varepsilon_0$ small. Bundle the bound:
For fixed $\varepsilon = 2$ and $z(0) \geq 0$, the exponential factor is at most $1$. Demanding the right-hand side be $\leq -\eta\,u^2$ for some $\eta > 0$ gives
Pinching on $z(0) \geq \log\varepsilon = \log 2$ (which we can enforce by a trivial vertical shift of the initial condition) reduces the bound to $-2 + 3\varepsilon_0 + 1 < 0$, i.e. $\varepsilon_0 < 1/3$.
The number $1/3$ is an algebraic artefact of the Gronwall estimate. It is what the worst-case absolute-value bound permits. It treats $+u$ and $-u$ identically — a symmetry that the original ODE does not respect.
Corollary 2.3 · Explicit basin from Gronwall
If $|r(0) - 1| < 1/3$ then $r(t) \to 1$ exponentially.
In particular, any $r(0) \in (2/3,\, 4/3)$ lies in the basin of attraction of $\Gamma$, and $|r(t) - 1| \leq |r(0)-1|\,e^{\mu t}$ for some $\mu \leq -\eta < 0$. The constant $\eta$ can be made explicit but is not sharp.
We integrate (1) with initial $\theta(0) = 0$, $z(0) = 0$, and vary $r(0)$. For each run we record the empirical contraction rate $\hat\mu$, defined as the slope of $\log|r(t) - 1|$ over $t \in [5, 20]$ (a window safely inside the linear regime once the trajectory has had time to approach $\Gamma$).
Outer column. Every $r(0) > 1$ converges. $\hat\mu$ is close to $-2$ and monotonically approaches it from above as $r(0) - 1$ grows (because the trajectory spends less time in the $e^{-z}$-perturbed regime). No value of $r(0) - 1$ up to $1.5$ misbehaves.
Inner column. $r(0) = 0.90$ converges. $r(0) = 0.80$ is on the edge — $\dot z$ brushes zero but the orbit survives. Below $r(0) = 0.80$ the trajectory drops vertically (negative $\dot z$), $e^{-z}$ explodes, the coupling term dominates, and $r$ leaves every neighbourhood of $1$ in finite time.
The asymmetry is not small. Gronwall said $r(0) \in (2/3,\, 4/3) = (0.667,\, 1.333)$. Reality says $r(0) \in (\,0.80\,,\, +\infty)$ for this range of $r(0) - 1$. The outer boundary from Gronwall is vacuous — there is no outer boundary at all in this window. The inner boundary is at $r_\star \approx 0.80$, which is stricter than the Gronwall guess of $2/3 \approx 0.667$. Gronwall would have declared $r(0) = 0.70$ safe; DOP853 says it collapses.
What goes wrong geometrically
At $r(0) < 1$, the Hopf term $r(1-r^2)$ pushes $r$ upward, good. But the contact coupling $\varepsilon(r-1)e^{-z}$ has the opposite sign — and worse, when $r < 1$ the vertical equation acquires a negative contribution $-\varepsilon(r-1)^2 e^{-z}$ (always negative). If $r$ starts too small, $\dot z$ can be overwhelmed; $z$ drops; $e^{-z}$ blows up; the coupling becomes a runaway. The Hopf term, bounded near $r=1$, cannot save us.
Geometrically: we lose positive invariance of $\{r > 0.80\}$ from below. We still have positive invariance of $\{r > 1\}$ from above (S1 board exercise). The ODE is asymmetric in $r=1$, and so is its basin.
§5 · See It on the Simulator
Live Numerical Demo
▶ dm³ Contact Flow — Watch the inner edge
Set $\varepsilon = 2$. Sweep $r_0$ from $0.85$ down to $0.75$. Somewhere between them the trajectory stops spiralling up and starts dropping. That is $r_\star$.
Guided demo (8 min)
$r_0 = 0.90$, $\varepsilon = 2$. Clean spiral up to $r = 1$. Note colour stays blue.
$r_0 = 0.80$. Trajectory flattens; there is a visible moment where the orbit hovers. Colour shifts toward gold then recovers.
$r_0 = 0.70$. Trajectory drops below the $r = 0.80$ ring (gold) and turns red. The $z$ readout starts decreasing.
$r_0 = 1.50$ for contrast. Converges fast. The outer basin has no problem.
§6 · What's Next
Hand-off to Session S3
We now have two numbers in tension:
$\varepsilon_0 = 1/3$ — what the textbook Gronwall inequality permits;
$r_\star \approx 0.80$ — what the actual flow does.
In S3 we translate the proof of Theorem 2.1 — the symmetric version — into Lean 4 / Mathlib 4. The formal skeleton is in AXLE (Chain.lean, SpiralReturn). The open obligation is the Lipschitz estimate on the coupling, tracked as AXLE Issue #12. We will walk the class through the statement, identify what is done, what is missing, and what a Lean-native sharper basin argument would look like. The sharp constant $r_\star$ is not in the Lean codebase — yet.
Board exercise · Take home for S3
Show that Gronwall cannot give $\varepsilon_0 > 1/3$ for this form of the estimate.
Pin $\varepsilon = 2$, $z(0) \geq \log 2$. Argue that the inequality $-2 + 3\varepsilon_0 + 1 < 0$ is tight — i.e. the coefficients $2, 3, 1$ are exactly what $r(1-r^2)$ and the coupling produce; there is no slack to recover. Conclude: any improvement must change the estimate, not tune its constants. This is precisely why the sharp inner boundary $r_\star$ requires a different proof technique — one that is sensitive to sign, not just magnitude.
The Gronwall bound is not wrong. It is coarse. A coarse bound is a loss of information. Locating that information — what a signed estimate could capture that an absolute-value estimate cannot — is open work. Theorem 2.1 (symmetric) is fully proved. Theorem 2.1* (sharp) is a project.