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

Formal statements and computational checks

The formal sources supplied with these manuscripts have not been rebuilt for this revision. Their recorded statements include the fixed counterexample for preconnected sets, the negation of the Formal Conjectures statement, its answer(False) form, and the total-variation formulation. The independent ordinary reconstruction in Section 2 uses Rouché’s theorem, the component degree and Hausdorff measure. Its Cayley signs, critical-disc estimates and all four Bernstein tests were recomputed with rational arithmetic in an earlier revision; the present edit retains those finite calculations. Independent human review of the construction and its correspondence with the 1958 wording is not recorded.

The $13/25$ calculation has the recorded full replay described in Section 4. Its analytic reduction is an ordinary proof and remains unformalised. The same distinction applies to the fourth-power mean estimate and the longer analytic family arguments. The numbered statements without a complete formal proof have therefore been retained as remarks, with their original mathematical content and local input notes. The following list records exactly what the existing formal deductions assume.

4.1.

No Lean proof covers the whole assertion. Lean checks the degree-two case, and the closing inequality $(13/25)e^X<1$ at the stopping time $X$ certified in the proof. The computation that certifies $X$, done by an exact-arithmetic program, and the analytic argument in degrees three and higher are not checked in Lean.

4.2.

The Lean proof assumes Remark 4.1.

4.4.

The Lean proof takes the separation bound (7) and the individual and summed bounds (8) as hypotheses; their derivation from the failure assumption, given in that section, is not checked in Lean.

4.5.

The Lean proof assumes Remark 4.1 in degrees above two; the degree-two case is checked without it.

5.1.

The Lean proof assumes the two-parameter bound (CF) in degrees $n\ge 3$, which the proof obtains by averaging over levels and value directions. The degenerate case, degree two and the numerical constants are checked without that input.

5.2.

The Lean proof assumes the bound (CF) from the proof of Remark 5.1, for a component containing at least $k_0$ roots; the rational inequalities are checked.

5.3.

The Lean proof assumes the averaging construction in the proof of Remark 5.1, rerun with the area–capacity inequality for the area of $C$; the rational cutoffs are checked.

5.6.

The Lean proof assumes the two-component split at the first critical level constructed in the ordinary argument: two one-root components whose closures meet at a critical point, each with boundary length at most $\beta \rho$ and each joining its root to that point within half its perimeter.

7.1.

The Lean proof assumes the ordinary analytic construction: the connector obtained through the square-root map, its Bergman length bound (7), and the capacity bound for the area of the two-sheeted component.

7.2.

The Lean proof assumes the same construction as Remark 7.1 for the second assertion. Inequality (6) and every numerical step are checked without it.

13.1.

No Lean proof covers the whole assertion. Lean checks the ray-disjointness, level-separation and saddle-scale steps of the proof; the Morse, monodromy and strip statements are not checked.

8.2.

The formal capacity conclusion takes as input the classical transfinite-diameter formula for a filled monic lemniscate. The root count at the first merger does not require that input.

No supplied proof establishes the reported Runge construction of unbounded one-root perimeters or the stronger assertion that every critical joining point fails in the near-pentagon example. Neither is used in the positive theorems. The fixed value of the degree-seven parameter is not a proof of the reported parameter family.