For z ↦ z² + c a fixed point satisfies z* = z*² + c, and the derivative there is λ = 2z*. Ask for the parameters at which that multiplier sits on the unit circle — λ = eiθ — and the answer falls out with no approximation:
That is the main cardioid. Not a curve resembling it, not a numerical fit — the boundary itself, parametrised by the argument of the multiplier. Across 400 angles the script finds |λ| − 1 and the fixed-point residual both below 1.11 × 10−16. The landmarks come out exact:
| internal angle θ | c | multiplier | event |
|---|---|---|---|
| 0 | 1/4 | +1 | cusp — saddle-node |
| π/2 | 1/4 + i/2 | i | root of the 1/4 bulb |
| 2π/3 | −1/8 + (3√3/8)i | e2πi/3 | root of the 1/3 bulb |
| π | −3/4 | −1 | period doubling |
The two ends of that table are the two real cases — a fold at λ = +1, a flip at λ = −1. Every angle strictly between them is a complex-conjugate pair crossing the unit circle, which in discrete time is the Neimark–Sacker bifurcation and in continuous time is Andronov–Hopf.
Scaling c by 0.99 and 1.01 about the origin moves it across the curve. Inside, the orbit of 0 settles onto the fixed point; outside, it does not.
| θ | |zn+1 − zn| inside | outside |
|---|---|---|
| 2π/3 | 3.79 × 10−15 | 2.98 × 10−1 |
| π/2 | 2.46 × 10−15 | 3.30 × 10−1 |
| 1.0 | 3.14 × 10−16 | divergent |
What makes this a Hopf-type event rather than a bare loss of stability is that the crossing carries a rotation number, and the rotation number is legible on the boundary. The bulb rooted at internal angle p/q carries an attracting cycle of period exactly q. Eight rationals, eight periods, no exceptions:
| p/q | root c | period found |
|---|---|---|
| 1/2 | −0.750000000 | 2 |
| 1/3 | −0.125000000 + 0.649519053i | 3 |
| 2/3 | −0.125000000 − 0.649519053i | 3 |
| 1/4 | +0.250000000 + 0.500000000i | 4 |
| 1/5 | +0.356762746 + 0.328581945i | 5 |
| 2/5 | −0.481762746 + 0.531656755i | 5 |
| 1/6 | +0.375000000 + 0.216506351i | 6 |
| 3/7 | −0.606356884 + 0.412399740i | 7 |
CardiacHopfReduction.lean reduces the three-variable oscillator ẋ = μx − ωy − xu, ẏ = ωx + μy − yu, u̇ = −Lu + (x²+y²) on the leading-order centre manifold u = (x²+y²)/L to a single radial equation. Block [5] checks the assertion independently of the Lean file, on two thousand random states:
The identity holds to 3.55 × 10−15; the derivative at the limit cycle is exactly −2μ, so the bifurcation is supercritical for every μ > 0, as the file’s header claims.
The rotation frequency ω does not appear in the radial equation at all. Whether ω is rational, irrational, Diophantine or Liouville makes no difference whatsoever to the amplitude, the stability or the existence of the limit cycle. Hold on to that sentence; section 5 is entirely about the fact that its discrete-time counterpart is false.
CardiacHopfReduction.lean compiles under the repository pin v4.32.0 and all four of its declarations report [propext, Classical.choice, Quot.sound]. The evidence lands in tools/verify-audit/<date>/geometry__CardiacHopfReduction.axioms.txt, and block [8] of the script reads the most recent one rather than a fixed date, so a re-audit cannot leave this sentence behind. What the audit does not do is repeat: the file is still outside every build target, so that result dates from the day it was run and nothing after it. Block [5] remains an independent check of the same algebra by a different route, which is worth keeping for the reason the kernel cannot supply — see below.
For a smooth map, whether a Neimark–Sacker crossing produces an invariant circle turns on a nondegeneracy condition and on the rotation number avoiding the low-order resonances. Beyond that, the arithmetic of the angle does not enter. In the holomorphic case it is the whole question. At an irrational internal angle the fixed point of z² + c is linearisable — a Siegel disk — or it is not, and which one happens depends on how well the angle is approximated by rationals.
Block [6] computes only the arithmetic, on numbers defined by their continued fractions so that the convergents are exact integers:
| rotation number | partial Brjuno sums |
|---|---|
| golden mean [0;1,1,1,…] | 0.000, 0.693, 1.243, 1.779, 2.195, 2.515, 2.750, 2.918 … 3.286 after 30 terms |
| built to diverge an+1 = ⌈eqn⌉ | 0.000, 1.386, 2.736, 3.760 — increments 1.386, 1.350, 1.024 |
The second construction forces every increment above 1 by choosing each partial quotient larger than eqn, so the sum diverges by construction rather than by observation. Two rotation numbers, the same map, the same normal form, the same codimension — and a classification that differs because of a number-theoretic property of the angle.
A Hopf intuition transports across the cardioid boundary at rational internal angle, where a period-q bulb attaches exactly where the multiplier says it should. At irrational angle it does not transport, and the obstruction is arithmetic. Section 4 makes the contrast sharp: in the continuous-time reduction the frequency cancels out of the radial equation entirely. The discrete case cannot cancel it, because there the frequency is the multiplier.
Nothing here proves any statement about irrational angles. Siegel’s theorem, Brjuno’s condition and Yoccoz’s converse are quoted. No orbit is integrated at an irrational angle, and deliberately so: a finite orbit cannot distinguish a linearisable fixed point from one that is not, and a script that appeared to do it would be measuring its own tolerance.
Two items remain on the Lean side and neither is mathematical. CardiacHopfReduction.lean is audited but untargeted, so a later regression would not fail the job; declaring it @[default_target] is what makes the audit repeat. And supercritical is a clean theorem whose statement, 0 < L → −(1/L) < 0, mentions no vector field — the identification of −1/L as the first Lyapunov coefficient is carried by its docstring and by nothing the kernel saw. The axiom gate cannot report that, because it reports axioms and not whether a statement earns its name. Section 4’s (d/dr)|r* = −2μ is the content the name claims, and it is a provable statement about the reduced field rather than about a reciprocal.
Five pages in this corpus already work with self-similarity and nesting, and each of them gains a different thing from the identification above.
Read beside WP-109, which found one word carrying two subjects and a theorem separating them above dimension two, this is the same shape with the separation moved: one normal form carrying two subjects, and an arithmetic condition separating them off the rationals.
2026-09-12. Section 4 and the footer first described CardiacHopfReduction.lean as not having been through the kernel, which was correct when written. The file was compiled and audited the same day under v4.32.0: four declarations, all on [propext, Classical.choice, Quot.sound], report committed under tools/verify-audit/2026-09-12/. Closing it required one tactic — field_simp left μ·r·(1−1) = 0 in limit_cycle and ring discharges it. The open items in section 5 were rewritten accordingly; the file is audited, not targeted.
sorryAx. A clean axiom report is not a reading of the statement: per R20, a theorem can assume its conclusion and still report clean. Follow the link before citing one as evidence.