An explicit rational lemniscate counterexample with certified separators
Jiang Yang, Xin Zhang
math.GN
Sep 23, 2026 · v1
TL;DR
The certified-separator counterexample construction is formalized in Lean 4 with Mathlib, with sources and verification logs archived on GitHub.
Abstract
In the setting of the previously reported degree-seven counterexample of ani, we present an explicit monic polynomial with real rational coefficients and a direct proof by certified separators. The polynomial has seven simple zeros in the open unit disk. Every continuous path joining distinct zeros in its closed unit sublevel set has image of one-dimensional Hausdorff measure greater than $2+10^{-8}$. Five piecewise-linear graphs exclude twenty of the twenty-one zero pairs; two short forbidden segments force a quantitative detour for the remaining pair. Exact rational Bernstein certificates verify the graph inequalities on forty-four terminal intervals and their unbounded tails. The proof does not require critical-point counting or analytic inverse branches. We separately record the general continuum and dilation arguments that transfer path-length obstructions to Hausdorff measure and to closed sublevel sets. Those transfers are not asserted as new principles. The focus is the explicit real-coefficient construction, its separation certificates, and its verified numerical margin, rather than a first negative answer to the length-two question or a disproof of every larger universal bound.
Problem
The question is whether every continuous path joining distinct zeros of a monic polynomial within its closed unit sublevel set must have length at most 2 (Erdős problem 1041 setting). A degree-seven counterexample by the contributor ani was previously reported; the authors give an explicit real-rational-coefficient version with a direct proof.
Approach
An explicit monic degree-seven polynomial with rational coefficients and seven simple zeros in the open unit disk is constructed. Five piecewise-linear graphs act as separators that exclude twenty of the twenty-one zero pairs. Two short forbidden segments force a quantitative detour for the remaining pair. Exact rational Bernstein certificates verify the graph inequalities on 44 terminal intervals and their unbounded tails, and the development is checked in Lean 4 with Mathlib, with its verification scope stated explicitly.
Results
Every continuous path joining distinct zeros in the closed unit sublevel set has one-dimensional Hausdorff measure greater than 2+10^{-8}. The proof avoids critical-point counting and analytic inverse branches. The Lean sources, exact certificates and verification logs are archived publicly.
