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

Unformalised remark: a quartic composed with a power map

We next examine the ordinary lifting argument based on Pendyala’s degree-four theorem [11] and four-point radial lemma [11]. The cited quartic result alone does not formalise this higher-degree construction. Let $P$ be a monic quartic, let $q\ge 2$ be an integer, and set

Assume that every root of $f$ lies in the open unit disc. A repeated root of $f$ gives the constant path, so suppose $f$ is squarefree. Then the roots of $P$ are distinct and nonzero. For a root $w=y^q$ of $P$, all points $h+{\zeta }^{j}y$, with $\zeta =e^{2\pi i/q}$, are roots of $f$. Hence the open-disc hypothesis gives

In particular $|w{|}^{1/q}=|y|<1$, which is the bound needed for the lifted length, and also $|w|<1$. Pendyala’s chord-or-radial argument supplies the quotient geometry in two cases. If two quotient roots satisfy $|w_i-w_j|<1$, every point $w$ of the chord $[w_i,w_j]$ lies in the unit disc; the two endpoint factors of $|P(w)|$ have product at most $|w_i-w_j{|}^2/4$ and the other two factors are below $2$, so $|P(w)|\le |w_i-w_j{|}^2<1$. Otherwise the quotient roots are pairwise at distance at least $1$. Choosing $R$ with $\underset{k}{max}|w_k|<R<1$ and applying the four-point radial lemma to the points $w_k/R$ gives distinct $i,j$ with $|P(t{w}_i)|\le R^4$ and $|P(t{w}_j)|\le R^4$ for $0\le t\le 1$, so the radial segments $[0,w_i]$ and $[0,w_j]$ lie in $\{|P|<1\}$. The extra issue is metric: a short chord in the $w$-plane need not lift isometrically through $y\mapsto y^q$.

Put $\alpha =1/q$. On a chord avoiding $0$, choose a continuous argument and hence a root lift $y$ with $y^q=w$. Differentiation gives $|dy|=\alpha |w{|}^{\alpha -1}|dw|$, independently of the chosen root. If the supporting line has distance $d$ from $0$, and $x$ is distance along that line from the perpendicular foot, then

The negative exponent is why replacing $|w|$ by $x$ gives an upper length bound. Lean checks the integral of the power-map derivative

If the foot lies on the chord, split there: the two integrals are bounded by the $\alpha$-powers of the distances from the foot to the endpoints, hence by $|a{|}^{\alpha }+|b{|}^{\alpha }$. If the foot lies outside the chord, integrate on one side of it; extending the interval to the foot bounds the result by the $\alpha$-power of the farther endpoint’s modulus. When the chord passes through $0$, choose a continuous root on each half and join the lifts at $0$; the integral is finite because $\alpha >0$. This proves the chord-lift estimate

The strict endpoint-length estimate also proves that if $0\le a,b<1$, $\alpha >0$, and a candidate length $L$ is at most $a^{\alpha }+b^{\alpha }$, then $L<2$. The close-pair chord therefore has a lift of length below $2$. In the other case the quotient arms meet at $0$, so their lifts are radial segments meeting at $h$, with total length $|w_i{|}^{1/q}+|w_j{|}^{1/q}<2$. In both cases $f=P\circ ((z-h{)}^q)$ transfers containment from the quotient curve. Distinct quotient endpoints give distinct roots of $f$. This proves the path assertion in every degree $4q\ge 8$. The fibre average gives a little more: $|h|<1$ and $|w_k{|}^{1/q}<\sqrt{1-|h{|}^2}$ for every quotient root. Consequently the same constructed path has length

This refinement concerns the translated power-substitution family, not arbitrary degree-$4q$ polynomials.

Pendyala proves the quartic geometric theorem and its four-point radial lemma. The local Lean module checks the antitone density inequality, its integral, the strict powered endpoint-length bound, and the final length estimate. It does not formalize Pendyala’s geometric lemma, the continuous covering-space construction of the root lift, or the ordinary chord/radial case assembly. This is a family defined by a power substitution, not a proof of unrestricted Erdős #1041.