The short paper develops the counterexample and the trinomial argument. Here Section 2 supplies the exact tests for the polynomial, while Sections 6 and 9 give further explicit paths. The area argument in Section 4 and the isolated-value construction in Section 7 are ordinary analytic proofs, still requiring formalisation. Their conclusions appear as remarks. The local notes identify the assumptions of the existing Lean deductions; Section C collects the formal and computational references.
The question and the degree-seven counterexample
A path estimate from area and boundary length
An isolated simple critical value
Examples separating the geometric hypotheses
Collinear roots and two sparse polynomial families
Further families and counterexamples to proposed proof steps
Separating the rays of critical values
Why the proposed spanning-tree estimate fails
Further questions about topology, length and perturbation
Numerical estimates for the packing inequality