\(\varepsilon_0=1/3\) is a symmetric, analytical, conservative guarantee: it is proved to hold uniformly regardless of direction. It is not the true basin boundary — it is a safe lower bound on it. The actual basin boundary, found numerically rather than by a general-purpose analytical bound, is asymmetric and closer to the attractor on the inner side than \(\varepsilon_0\) alone would suggest.
certify_rstar.py — a deterministic bisection search over initial radius \(r_0\), combined with high-precision (rtol \(10^{{-12}}\)) DOP853 integration of the exact toy-model ODE from Week 2. For \(r_0 > r^*\), trajectories converge to \(\Gamma\) (\(r\to1\), \(z\to+\infty\)); for \(r_0 < r^*\), they escape (\(r\to0\), \(z\to-\infty\)). The script’s own comment is precise about the relationship to \(\varepsilon_0\): “the Gronwall estimate predicts the inner boundary at \(2/3 \approx 0.667\); the true boundary \(r^*\approx0.776\) lies strictly above \(2/3\).” The conservative bound underestimates how much of the basin is actually safe.
The same value is recorded directly in Lean, Dm3Arithmetic.lean: noncomputable def r_star : ℝ := 0.77594059, with r_star_pos and r_star_lt_one proved (i.e. \(r^* \in (0,1)\) is machine-checked). What is not proved: Chain_updated.lean states inner_basin_is_asymmetric as an axiom explicitly marked “pending dm³ ODE formalisation.” Read carefully, this is two separate epistemic claims layered together — (1) this specific numeric boundary is real and reproducible (strong evidence, computational, not formal-proof), and (2) the basin is asymmetric in general, as a theorem about the ODE’s structure (currently asserted, not derived).
Geometrically: the outer Gronwall ball (\(\varepsilon_0=1/3\)) is a sphere around \(\Gamma\) in the toy model’s state space, valid in both directions from the attractor. The true basin is not a sphere — it extends further on the outer side than the inner side, which is exactly what “asymmetric” means here. Trajectories that undershoot \(r=1\) have less room before they’re lost to \(r\to0\) than trajectories that overshoot.
-- dm³ 102 · Week 03 · basin geometry, certified vs axiomatic -- CERTIFIED (numerical, 8dp, reproducible): -- r* = 0.77594059 (certify_rstar.py — bisection + DOP853, rtol=1e-12) -- Dm3Arithmetic.lean: r_star := 0.77594059 -- r_star_pos, r_star_lt_one -- proved -- STILL AN AXIOM (Chain_updated.lean): -- inner_basin_is_asymmetric -- "pending dm³ ODE formalisation" -- ε₀ = 1/3 (conservative, symmetric) vs r* ≈ 0.776 (true, asymmetric) example : (1:ℝ)/3 < 0.776 := by norm_num