Paths in Polynomial Lemniscates: A Degree-Seven Counterexample and Radial Connections

Certificate.

The comparison gives an upper bound $X$ on the logarithmic time needed for the forced area to exceed $1$. It therefore gives a contradiction whenever $\mu e^X<1$. The stated constant $13/25$ is a convenient rational choice with room to spare, not an optimality claim. A program evaluates every accepted inequality in exact rational arithmetic, with directed rounding on the transcendental evaluations. Its fixed rational brackets for $\pi$ and $\log 2$ have different elementary checks: Machin’s identity $\pi =16\arctan (1/5)-4\arctan (1/239)$ for the former, and $\log 2=2\sum _{j\ge 0}{3}^{-(2j+1)}/(2j+1)$ for the latter. Alternating-series bounds and a geometric tail bound, respectively, suffice to verify them. Its full run uses $18$ area-table levels, $14$ radii in each weighted bound, $126$ attempted choices of weights, maximum step $1/400$, and the initial lower area ${10}^{-6}$ at $x=3/{10}^5$. Only accepted rational certificates enter the comparison; its early steps may be shorter than $1/400$. The full run certifies

which gives Remark 4.1. The full replay recorded on 29 September 2026 used the immutable program cited above. It accepted all $126$ dual certificates and reproduced this value of $X$; no new replay is claimed for the present editorial revision. The retained certificate data give the exact radii and nonnegative weights, together with their sums and certified upper bounds. The program’s Git blob identifier is e9b4998884575a31ce0d1f6762a210ae2d617103. That replay also ran the comparison regression and the observer-containing-circle audit. The comparison check is exact; the geometry audit combines an exact full-circle boundary test with floating identity checks. No new per-degree thresholds were computed.

A coarser run gives $X=664373027131/1000000000000$ and the weaker threshold $51/100$. The floating optimiser proposes weights but supplies no proof. The argument uses only the subsequently certified rational bounds on their sum and on the supremum $U$. Each accepted pair supplies a weight sum $\mathrm{\Sigma }$ and a certified upper bound for the supremum $U$ in Remark 4.4. For orientation, the pairs of the coarser run at $a=1$, rounded to six decimal places, are $(0.085674,0.045865)$, $(0.126361,0.021829)$, $(0.163157,0.010513)$ and $(0.208928,0.004318)$, giving $kU+\pi \mathrm{\Sigma }$ approximately $0.4526$, $0.5716$, $0.6808$ and $0.7945$ at $k=4,8,16,32$, respectively. These rounded pairs do not themselves certify an inequality; the comparison uses the unrounded rational values and their directed bounds. To bound the supremum over $d$, the checker subdivides intervals and bounds each term in the direction needed for an upper bound. The function $\lambda$ is decreasing. For fixed $r$, the slice angle $w(d,r)$ has no strict interior minimum. Indeed, before clipping the angle to $0$ or $\pi$, its cosine is

The numerator of $H^{\prime }$ is increasing. Thus $H$ has at most one interior minimum, and $w=\arccos H$ has at most one interior maximum; clipping preserves the endpoint-minimum property. On an interval $[d_{-},d_{+}]$, therefore,

Beyond $d=\underset{i}{max}{r}_i+D/2$, all the slice angles vanish, so only the decreasing function $\lambda$ remains. These are interval bounds, not values sampled on a grid. The closing inequality is independently checkable: with $X=635762889599/{10}^{12}$ and $e^X\le \sum _{j\le 14}{X}^j/j!+(X^{15}/15!)/(1-X/16)$, rational arithmetic gives $(13/25)e^X<0.982000386<1$. The same majorant also gives

Thus the full certificate in fact gives the path conclusion for $\mu \le 529/1000$, without changing the geometric argument or its hypotheses. This is an arithmetic consequence of the certified stopping time. We retain $13/25$ in the theorem and its scaling corollaries as the simpler constant.