Plectis
Erdős problem #1041

Short connections inside polynomial lemniscates

Must two roots of a monic polynomial in the open unit disc be joined by a sub-two-length curve inside its unit lemniscate? Ani’s degree-seven example refutes the exact Formal Conjectures statement; correspondence with the 1958 wording awaits human review.

Formal statement refuted Problem on GitHub

The problem

The question

Put n≥2 roots strictly inside the circle of radius 1 about 0, and form f(z)=(z−z1)⋯(z−zn). This is monic: its leading coefficient is 1. At a point z, |f(z)| is the product of its distances to the roots. Call a point allowed when that product is less than 1.

Any two roots are less than 2 apart in a straight line. The question is whether some pair can always be joined in under 2 while staying entirely on allowed ground.

An example

For f(z)=z2−0.81, the roots are −0.9 and 0.9. Between them, |f(x)|=0.81−x2≤0.81<1. Their whole straight segment is therefore allowed, and its length is 1.8. This polynomial answers yes; the question asks whether every permitted polynomial has such a path.

Let f(z)=∏i=1n(z−zi)∈C[z] with |zi|<1 for all i. Must there always exist a path of length less than 2 in {z:|f(z)|<1} which connects two of the roots of f?

The setup in detail

A complex number z=x+iy is a point (x,y) in the plane. Its modulus |z|=x2+y2 is its distance from 0; |z−w| is the distance from z to w. Multiplication multiplies moduli, so

|f(z)|=|z−z1|⋯|z−zn|.

The allowed region is therefore specified entirely by the roots: multiply the distances to all of them and ask whether the answer is below 1. Every root is allowed, since one factor is zero. The leading coefficient must be 1; multiplying the polynomial by a large constant would change the region.

A path is a continuous curve, and its length counts the whole distance travelled. The straight distance between any two roots satisfies |zi−zj|≤|zi|+|zj|<2. The issue is containment: a short straight segment may cross forbidden ground. The question asks for at least one suitable pair, for every permitted polynomial. Two occurrences of a repeated root give a constant path of length zero, so a counterexample must have distinct roots.

ani’s fixed degree-seven polynomial answers this precise question no. The paper proves the stronger statement that every connected subset of its allowed region containing two roots has one-dimensional Hausdorff measure greater than 2. This measure counts length of a set without choosing a route through it; a path’s travelled length is at least the measure of its image.

Erdős, Herzog and Piranian posed the historical question in 1958, and Pendyala proved the degree-four case. ani posted this counterexample in September 2026. The supplied Lean sources verify the stated total-variation and Hausdorff-measure formulations. Independent human review of their correspondence with the 1958 wording is not recorded. The proof fixes one polynomial; ani’s wider small-parameter family is not proved here.

The example in detail

For f(z)=z2−0.81, a path between the real roots −0.9 and 0.9 must cross the imaginary axis: its horizontal coordinate changes continuously from negative to positive. On that axis write the crossing point as iy. Then

f(iy)=−y2−0.81,|f(iy)|=y2+0.81.

Thus the only allowed crossings have y2<0.19, or |y|<0.436…. This vertical interval is a passage that every allowed root-to-root path must cross.

Reaching a crossing iy from either root costs at least the straight distance 0.81+y2. Hence the whole path has length at least 20.81+y2. At y=0 this is 2×0.9=1.8, and the horizontal segment achieves that length while staying allowed.

Moving the roots closer to the unit circle makes the passage narrower, but the horizontal segment still works. A narrow passage alone is therefore insufficient for a counterexample. The seven-root construction also puts its passage where reaching it from the two roots already costs more than 2.

Erdős #1041. Left: the unit circle, dashed, and the region where ani's degree-seven polynomial has modulus less than 1: seven hatched petals meeting near the centre, one root in each. The roots A and B and their petals are red; the dashed chord between A and B is 1.95 long and leaves the region. Right: the centre magnified, the disc of radius 1.3 times 10 to the minus 12. Only the arms of A and B reach it, and they join at the passage P, 0.82 times 10 to the minus 12 above the centre 0. Red lines leave P towards A and B: every path from A to B passes P, and the distances from A and B to P add up to more than 2. Dashed lines leave 0 towards A and B: the distances to the centre add up to just under 2, but the line towards A crosses empty ground, where the modulus exceeds 1, so that route leaves the region. 1.95 A B 2 A B 0 P 0.82 × 10−12 |f| > 1 |f| < 1 |z| < 1.3 × 10−12 |A − P| + |P − B| > 2 |A − 0| + |0 − B| = 2 − 2 × 10−96

The crux

The hatched petals are allowed ground in ani’s seven-root counterexample; blank ground is forbidden. Only the red roots A and B lie in the same connected piece. Their dashed straight segment is 1.95 long but leaves the hatching.

The right-hand circle magnifies the centre. The red passage P lies slightly above 0: every allowed A-to-B path must pass extremely close to P. That tiny detour makes every such path longer than 2. The result below explains the length bound.

The drawing uses two scales because the roots are about one unit from 0 while the passage is only about a trillionth of a unit away. Hatching always means allowed points, and red always marks the two arms containing A and B.

  1. Start with seven petals. The polynomial z7−1 has seven roots evenly spaced on the unit circle. Its allowed region has seven petals whose boundaries touch at 0; 0 itself is forbidden. ani changes its coefficients slightly and moves every root to distance ρ=1−10−96 from 0, strictly inside the circle. These changes are invisible in the left view but alter how the petals meet.
  2. Find the only pair that can be joined. The paper verifies that five connected pieces contain one root each and the sixth contains A and B. Paths cannot jump between pieces, so only this pair needs a length estimate.
  3. Locate every possible crossing. On the two-root piece, each ordinary polynomial value has two preimages. Cutting the disc of values along a suitable segment separates these into a side containing A and a side containing B. Any joining path must cross the preimage of the cut. A local quadratic estimate places that whole passage within ρε/3750 of P, where ε=10−12. Enclosing the whole passage rules out an alternative crossing farther away.
  4. Pay for reaching the passage. The paper’s root enclosures give |A−P|+|B−P|>ρ(2+0.143ε). Moving the crossing away from P can reduce each distance by at most the passage’s enclosing radius. Therefore every allowed joining path has length greater than ρ(2+(0.143−2/3750)ε)>2. The excess is tiny but strictly positive.

The dashed route through 0 would cost |A|+|B|=2ρ<2, but part of it crosses blank ground. The close-up shows why moving from 0 to the compulsory passage matters. Its contours approximate the region at drawing precision; exact rational inequalities in the paper establish the bound. The result panel below replaces the tiny passage by a larger enclosing disc so that this same length obstruction is visible.

The region where ani's degree-seven polynomial has modulus below 1: seven hatched petals inside the unit circle, one zero in each, with the zeros A and B in red, 1.95 apart, joined by red legs through the centre, and the dashed ellipse on which the distances to A and B add up to 2, passing through the centre. Beside it, the disc of radius 1.2 times 10 to the minus 12 about the centre: the arms of A and B meet at a passage just beyond the ellipse, now a dashed line; a small red circle C encloses the passage, and red rays leave it towards A and B. Reaching C from A and from B costs more than 2, so every path joining two zeros is longer than 2. 2 1.95 A B |z| < 4.4 × 10−12 0 < 2 > 2 C > 2 |z| < 1.2 × 10−12 ws dist(A, C) + dist(B, C) > 2 C: |w − 4i/5| ≤ 1/10

ani’s degree-seven polynomial has seven distinct roots strictly inside the unit circle, yet no pair has an allowed joining path of length at most 2. The dots are roots; the hatching is allowed ground, where |f(z)|<1 (the product of distances to the roots). A connected piece is one that can be traversed without leaving allowed ground. Only the red roots A and B share a piece. They are 1.95 apart; the close-up shows where their two red arms join. Try the red broken line through the centre 0: its two legs total just under 2. More generally, visiting any point z costs at least |A−z|+|z−B|, the two straight distances to it. The dashed ellipse is the set of points where |A−z|+|z−B|=2. A path of length at most 2 must stay inside this boundary. The close-up magnifies it until it looks straight. Every allowed A-to-B path must cross the tiny passage inside the red disc C. The entire disc lies beyond the dashed boundary. C encloses the passage; it is deliberately wider than the passage itself. The distance from A to C plus the distance from B to C already exceeds 2. Even free travel inside C cannot fit the budget. The short route through 0 fails because it leaves allowed ground.

Theorem 1.2 proves the stronger claim that every connected subset of the allowed region containing two roots has one-dimensional Hausdorff measure greater than 2. This measures the length of a set, independently of a path tracing it, and is at most the travelled length of such a path. Five connected components contain one root each; only the sixth contains A and B. Write these roots as A=ρζ3, B=ρζ6, with |ζj|=1, ρ=1−10−96 and ε=10−12.

Why must a path reach C? On the two-root component, each ordinary value in the unit disc has two preimages. Cutting that value disc from its unique critical value to the boundary separates the preimages into two open regions, one containing each root. A joining path must cross the preimage of the cut. The paper’s Lemma 2.1 confines this whole passage within ρε/3750 of the critical point cs=ρεws, where |ws−4i/5|<1/40. Consequently it is enclosed by the drawn disc C={z:|z−c|≤ρε/10}, centred at c=(4/5)iρε.

The verified root enclosures imply Im⁡(ζ3+ζ6)<−1/3. Projecting the two root-to-centre vectors onto their respective root directions gives |A−c|+|B−c|>ρ(2+4ε/15). Subtracting the two disc radii yields dist⁡(A,C)+dist⁡(B,C)>ρ(2+ε/15)>2. For a connected set, radial projection on each of the two disjoint open regions gives the corresponding measure bound; those contributions can be added. The contours in the close-up approximate the allowed region; the inequalities, rather than the plotted pixels, prove the obstruction.

The supplied Lean sources cover arbitrary preconnected sets, the negation of the Formal Conjectures statement, and path total variation. This is one fixed polynomial: ani’s small-parameter family is not proved here. Independent human review of the match with the original 1958 wording is not recorded. This drawing supplies no new Lean replay.

The region where the quartic z^4 + (6/5) r^2 z^2 + r^4, r = 0.999, has modulus less than 1: an hourglass pinched at the origin, with its four zeros just inside the dashed unit circle. Straight segments join every zero to the origin inside the region; the red pair, of total length 1.998, joins two zeros. Beside it, the unit disc of values: the red segments map to a red leaf from b to 0 inside two triangles with vertices 0, b and minus zeta to the fourth. f ζ1 ζ2 1.998 −ζ14 −ζ24 0 b values of f

The hatched region is where f(z)=z4+65r2z2+r4, with r=0.999, has modulus below 1. Along the segment from 0 to a zero ζ, the value of f is an average of b=r4, −ζ4 and 0 with nonnegative weights. All three lie in the unit disc on the right, so every such segment stays in the region, and the red path between two zeros has length 1.998.

The quartic is the trinomial factor of the sextic in the record’s Example 3.2, with the radius r=999/1000 used there; its zeros (r/5)(±1±2i) have modulus r. Its critical values r4 and 1625r4 lie inside the disc, so {|f|<1} is one piece, pinched at the origin where f(0)=r4=0.996. The root equation removes the middle term: f(tζ)=(1−t2)b+(t2−t4)(−ζ4)+t4⋅0, with nonnegative weights summing to 1, so along the segment to ζ1 the values run from b=f(0) to 0=f(ζ1) inside the triangle with vertices 0, b and −ζ14=r4(7+24i)/25. The mirror arc belongs to ζ2=ζ¯1, and since f is even the blue segments take the same values. The path ζ1→0→ζ2 has length 2r=1.998. The same identity, with tm and tn, proves the theorem for every monic trinomial zn+azm+b with its zeros in the open disc; the paper claims no novelty for this argument.

Results and open questions

#1041. A source-backed ordinary theorem covers monic degree-n polynomials, n≥3, whose distinct zeros lie on a circle of radius ρ and satisfy 2ρn≤1: two adjacent zeros have chord length at most 2ρsin⁡(π/n)<2, and their straight chord lies in {|f|<1}. A repeated zero is an immediate short connection. The reasoning record explains the alternation and chord argument. The proof is outside Lean; an exact finite checker tests load-bearing identities and configurations, and the theorem does not yet have a curated claim row. At each fixed degree, the sharp arc constant 2 leaves radii sufficiently close to 1 outside this method.

Every monic trinomial with roots in the open unit disc also has radial root-to-origin segments inside {|f|<1}, so any two roots join through the origin with length less than 2; Lean checks the complete displayed trinomial statement. For collinear roots, Lean checks a sharp Chebyshev segment bound and the resulting <2 connector when the roots lie in the open unit disc. These are solved families, not a general connector theorem. For a squarefree monic polynomial, write μ=minf′(c)=0|f(c)|. An ordinary theorem gives a connector of length less than 2 in the open unit lemniscate whenever μ≤13/25, with no root-location hypothesis; scaling gives a connector of length less than (5/2)μ1/n in {|f|<(25/13)μ}. The sharp critical-value mean on the closed unit disc is Lean-checked with source-bound audit evidence, and the paper also gives an ordinary proof. The mean controls critical values, not connectors.

A further ordinary theorem gives a connector of length less than 2 in every degree n≥3 when a simple nonzero critical value admits the stated separated critical-value disk at radius 4/3; it asserts no existence of such a disk. On the generic stratum where simple nonzero critical values have pairwise distinct arguments and moduli, an ordinary slit-sheet theorem identifies the inverse-ray root-connection tree but gives no uniform length bound. Lean checks Newton-flow decay, ray-separating translations, and perturbative root retention. Using one degree-seven polynomial constructed by the erdosproblems.com contributor ani, Lean proves that every preconnected strict-lemniscate set joining two distinct roots has one-dimensional Hausdorff measure greater than two.

This refutes the exact Formal Conjectures path-image-length statement and the separate total-variation formulation; correspondence with the 1958 wording remains unreviewed. The short paper also gives a cubic showing why a two-root first merger alone does not force a capacity gap; its Lean capacity clause assumes the classical transfinite-diameter formula. Read the short paper, long record, and selected formal checks.

Read the public result guide

Short paper, 19 pages

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

In this paper

Introduction

Two points in the open unit disc are less than 2 apart. The extra condition in the following question is that the whole connecting curve stay where a given polynomial has modulus less than 1. For a monic polynomial f, write

Ωf={z:|f(z)|<1},Kt(f)={z:|f(z)|≤t}.

Erdős, Herzog and Piranian [2] asked whether two zeros in the open unit disc could always be connected by a short curve in Ωf. Their question is listed as Problem 1041 in Bloom’s catalogue [1].

Problem 1.1 (Erdős #1041). Let f(z)=∏i=1n(z−zi) be monic with n≥2 and all zi in the open unit disc. Must two root occurrences be joined by a curve of length less than 2 inside {|f|<1}?

A repeated root allows a constant curve between two occurrences, so we consider distinct zeros. Pendyala [4] proved the degree-four case using a close-pair chord or radial segments through the centre of a smallest enclosing disc. In degree seven the answer is negative. The example was constructed by the erdosproblems.com contributor ani.

Theorem 1.2 (ani’s degree-seven example). The monic polynomial f in (2) has seven distinct zeros in the open unit disc. Every connected set K⊂Ωf containing two of its zeros satisfies H1(K)>2.

Here H1 is one-dimensional Hausdorff measure. A rectifiable path image has measure at most its total variation, so the theorem excludes short paths as well as more general connected sets.

Five components of Ωf contain one zero each; the sixth contains two and is the only possible place to join a pair. On this component, f has degree two. Cut the value disc from its critical value to the unit circle. Inside the two-root component, the whole slit preimage lies in a small disc about the critical point. Connectedness forces a root-joining set to approach this disc on both inverse sheets. The two radial projections then give a lower bound: the sum of the root distances from the critical point, minus twice the small disc’s radius. For the chosen pair this bound exceeds 2.

Section 2 contrasts the quadratic with the counterexample; Section 3 treats trinomials and the obstruction introduced by a fourth term. Section 6.1 separates root proximity from containment. Sections 4 and 5 construct paths by component growth and continuation around an isolated critical value, respectively. These independent analytic arguments remain unformalised. The companion paper gives their proofs, the counterexample’s rational data, and the arguments behind the later estimates and questions.

A component with a narrow bottleneck

A quadratic model

Consider p(z)=z2−r2 with 0<r<1. Its critical point is 0, its critical value is −r2, and the outward slit in the value disc is J=(−1,−r2]. We can compute its preimage without choosing a branch:

p−1(J)={iy:|y|<1−r2}.

This vertical interval separates the two inverse sheets containing r and −r. It shrinks to the critical point as r↑1. Yet the horizontal segment [−r,r] stays in {|p|<1} and has length 2r<2. A narrow neck alone therefore does not give the desired counterexample. For the radial-distance estimate below to exceed 2, the two root distances from the critical point must themselves have sum greater than 2.

A length estimate for a double cover

The degree on a component counts preimages in that component, with multiplicity; it equals the number of zeros there, not necessarily the degree of the polynomial [8]. Near a simple critical point c, write p(c+z)−p(c)=z2A(z). The quadratic model suggests a spatial scale δ/M: the value slit has length δ=1−|p(c)|, while M=|A(0)|=|p″(c)|/2 converts squared distance into value distance. The next lemma controls this comparison on a disc of radius h. Degree two serves a different purpose. It ensures that the two local preimages near c exhaust every fibre in the chosen component, so a connection cannot pass through an unexamined part of the slit preimage.

Lemma 2.1. Let p be a polynomial and U a component of {|p|<1} on which p has degree two, with one simple critical point c and v=p(c)≠0. Write p(c+z)−v=z2A(z) and put M=|A(0)|, δ=1−|v|. Let h>0. If |A(z)/A(0)−1|≤1/4 for |z|≤h and δ<Mh2/4, then every connected subset K of U containing its two roots a,b satisfies

H1(K)≥|a−c|+|b−c|−83δ/M.

Proof. Cut the value disc along J={tv:1≤t<1/|v|}. The slit avoids 0 and removes the only critical value of p|U. Over its simply connected complement, the double cover splits into two inverse sheets U1,U2, containing a,b respectively.

The sheet boundaries inside U lie over the slit. To confine them, put r0=(4/3)δ/M<2h/3. The relative-error hypothesis makes A nonvanishing on this disc, and on |z|=r0 gives

|p(c+z)−v|≥34Mr02=43δ>δ.

Every value on J is less than δ from v. Rouché’s theorem compares its preimages with the double zero of p−v and gives exactly two in B(c,r0), counted with multiplicity. As the value moves from v along J, these preimages continue from c without crossing the circle. Their values stay in the unit disc, so they remain in U. The degree-two hypothesis now identifies these local preimages with the entire fibre in U. Thus

p−1(J)∩U⊂B(c,r0).

It remains to count how much of K lies on each sheet. For r0<t<|a−c|, suppose K∩U1 missed the circle |z−c|=t. Then K∩U1∩{|z−c|>t} would be both open and closed in K: the boundary of U1 inside U lies in B(c,r0), and the remaining boundary is on the missing circle. This set contains a and excludes b, contradicting connectedness. Hence the radial image of K∩U1 contains (r0,|a−c|) whenever this interval is nonempty. The map z↦|z−c| is 1-Lipschitz, and therefore

H1(K∩U1)≥(|a−c|−r0)+.

Here x+=max(x,0). The same argument on U2 gives the contribution from b. The radial intervals may overlap on the real line; it is the disjointness of the sheets in the plane that permits addition. Hausdorff outer measure adds across disjoint open sets, without a measurability assumption on K, so

H1(K)≥(|a−c|−r0)++(|b−c|−r0)+≥|a−c|+|b−c|−2r0.

This is the required bound. No parametrisation of K has been used. ◻

This figure is drawn in the PDF.

The polynomial

Starting from z7−1, we put the roots on |z|=ρ<1 and split the multiple critical point at scale ε. The linear, quadratic and cubic perturbations below all have order ε7 at z=εw, so they alter the critical geometry without comparable root displacement. We must identify the only component containing a pair and make its distance surplus exceed the loss in Lemma 2.1. The fixed coefficients are those of ani’s construction. Put s=10−6, ε=s2=10−12 and ρ=1−s16, and let

A=−3295071600,B=551827800,C=−2301381332000,a=A−is,b=iB+95s,c0=−C−16225is.

Define

(1)F(z)=z7−1+ε4(az3−a¯z4)+ε5(bz2−b¯z5)+ε6(c0z−c¯0z6),(2)f(z)=ρ7F(z/ρ).

Putting the roots on a circle.

By F(z)=−z7F(1/z¯)―, the Cayley substitution z=(1+ix)/(1−ix) gives a real polynomial after clearing the denominator and removing a constant phase. Symmetry alone does not locate the zeros: the decisive step is seven sign changes on disjoint rational intervals. The map parametrises the unit circle except −1, so these give seven distinct circle zeros ζj, exhausting the degree. Thus −1 is not a zero and bj=ρζj satisfies |bj|=ρ<1. The distance estimate below absorbs the contraction 1−ρ=ε8.

Resolving the critical points.

At the smaller scale z=ρεw, write

F(εw)=−1+ε7Q(w),Q(w)=c0w+bw2+aw3−εa¯w4−ε3b¯w5−ε5c¯0w6+w7.

Rouché estimates on six disjoint rational discs locate the six zeros of Q′. Exactly one, ws, corresponds to a critical value of modulus less than one. It satisfies

|ws−(0.0000000039+0.8232474662i)|<10−6.

Let cs=ρεws, v=f(cs), δ=1−|v|, and write f(cs+z)−v=z2As(z). Since |ζj|=1,

|bj−cs|=ρ|ζj−εws|≥ρ(1−εRe⁡(wsζ¯j)).

The negative projection sum for ζ3,ζ6 gives a positive distance surplus of order ε; the contraction has only order ε8. The exact bounds at the fixed parameter are:

(3)M:=|As(0)|>180ρ5ε5,δ<365⋅106ρ7ε7,(4)|As(z)/As(0)−1|<14(|z|≤ρε10),|b3−cs|+|b6−cs|>ρ(2+1431000ε).

The subscripts 3,6 refer to Cayley roots in the intervals (43812,43813)/104 and (−4816,−4815)/104. The Taylor bound gives the lemma’s quadratic control, while the bounds on M and δ give δ/M<ρε/5000. Thus the slit loss is smaller than the displayed distance surplus. This comparison matters only if the selected roots share a component; the following paths establish that membership, not a short connection.

Identifying the two roots in the component.

In the w-plane, polygonal arcs connect a small disc about ws to points near 8ζ3 and 8ζ6. Short joining segments then reach those exact root directions, and radial segments continue to the roots. For the four inner polygonal segments we use

1−|f(ρεw)|2≥2ρ14ε7(7ε+Re⁡Q(w)−12ε7|Q(w)|2).

This follows by expanding the square and using 1−ρ14≥14ρ14ε8. On each segment, the expression in parentheses is a polynomial of degree at most fourteen in the segment parameter. All fifteen coefficients in its degree-fourteen Bernstein basis are positive. The basis polynomials are nonnegative and sum to one, so the expression is positive along the whole segment, which therefore stays inside {|f|<1} after scaling. The companion bounds Q directly on the short joining segments. For the radial portions we use the root identity

F(tζ)=t7−1+∑k=16ε7−kqkζk(tk−t7),Q(w)=∑k=17qkwk,

which gives |F(tζ)|<1 for 8ε≤t≤1. All rational intervals, vertices and coefficient tests are specified in the companion’s finite verification. At the regular level |f|=1, the component-wise Riemann–Hurwitz calculation [8] gives k−1 critical points in a component with k zeros, counted with multiplicity. Since cs is the only critical point in Ωf, its component contains exactly the two roots just reached; every other component contains one.

Proof of Theorem 1.2. Apply Lemma 2.1 to the component containing b3,b6, with h=ρε/10>0. The finite estimates give δ/M<ρε/5000 and δ<Mh2/4. Every connected set in that component containing the two zeros therefore has measure greater than

ρ(2+(1431000−815000)ε)>2.

All other components contain one zero. A connected set containing two zeros must lie in the component just considered, which proves the theorem. ◻

The choice s=10−6 is fixed throughout. Extending these estimates to the small-parameter family reported by ani remains unproved here. The argument estimates the measure of the connected set itself; a bound for the total variation of a chosen parametrisation would not suffice.

Trinomials and radial segments

If f(z)=zn+b has a zero ζ in the open unit disc, then |b|=|ζ|n<1. The identity f(tζ)=b(1−tn), 0≤t≤1, keeps the whole segment [0,ζ] in the lemniscate. The same cancellation survives a middle monomial. Its coefficient may be large, so we use f(ζ)=0 to eliminate that term before taking absolute values. The remaining quantities are b and −ζn, both of modulus less than one.

Theorem 3.1 (all-degree monic trinomials). Let 1≤m<n and

f(z)=zn+azm+b,

with every zero in the open unit disc. For any zero ζ, the entire segment [0,ζ] lies in {|f|<1}. Distinct zeros ζ1,ζ2 are therefore joined by the broken line ζ1→0→ζ2 of length ‖ζ1‖+‖ζ2‖<2 inside the open unit lemniscate.

Proof. Fix a zero ζ. Eliminating aζm with the root equation gives

f(tζ)=(1−tm)b+(tm−tn)(−ζn).

Vieta’s formula gives |b|<1. For 0≤t<1, the two weights are nonnegative, the first is positive, and their sum is 1−tn. Hence

|f(tζ)|≤|b|(1−tm)+|ζ|n(tm−tn)<1−tn≤1.

At t=1 the value is zero. We join any two distinct zeros by concatenating their segments through the origin. ◻

Abel summation identifies exactly what this argument needs. For f(z)=∑k=0nakzk and a zero ζ, put Sj=∑k=0jakζk. Since Sn=0, summation by parts gives

f(tζ)=∑j=0n−1(tj−tj+1)Sj.

For 0≤t<1, the weights are nonnegative and sum to 1−tn. Thus f(tζ)/(1−tn) is a convex combination of the Sj. For a trinomial, Sj=b before the middle term and Sj=−ζn after it. Thus every partial sum lies in the unit disc. A fourth term introduces another partial sum for which root locations alone need not give that bound, as the next example shows. The conclusion concerns segments ending at zeros, not star-shapedness of the whole lemniscate.

Proposition 3.2 (failure of a prescribed radial segment). There exist r∈(0,1) for which every zero of

fr(z)=z6+15r2z4−15r4z2−r6

lies in the open unit disc, yet the radial segment from the origin to the zero r leaves {|fr|<1}.

Proof. We substitute z=rw and factor the polynomial as r6(w2−1)(w4+65w2+1). The quadratic in w2 has conjugate roots of product one, so all six original zeros have modulus r. At the midpoint of that segment, fr(r/2)=−(327/320)r6; choosing 320/327<r6<1 proves the assertion. ◻

This failure concerns the prescribed segment only. In Section 6.2 we use the partial-sum identity again, first for power substitutions in a cubic and then for a quintic whose two missing coefficients select a suitable pair of segments.

A small least critical value

A small critical value leaves a long interval of levels before the unit lemniscate is reached. For a squarefree polynomial, put μ=minf′(c)=0|f(c)|>0 and follow a component from its first merger at level μ to level 1. If no two roots admit a connection shorter than 2, conformal length estimates force them far apart in the component’s hyperbolic metric. Packing then bounds the root count from below; inverse-ray averaging turns that count into a lower bound for area growth. When log⁡(1/μ) is large enough, this growth contradicts Pólya’s area bound.

The companion proves the analytic reduction and gives the rational comparison. The resulting criterion needs no restriction on root locations, but its analytic proof has not been formalised.

Remark 4.1 (unformalised small-critical-value assertion). Let f be squarefree and monic of degree n≥2, and let μ be its least critical-value modulus. If μ≤13/25, then two distinct roots are joined inside {|f|<1} by a rectifiable curve of length strictly less than 2.

Remark 4.2 (scaling of the preceding assertion). Every squarefree monic polynomial of degree n≥2 has two distinct roots joined in {|f|<(25/13)μ} by a curve of length less than

2((25/13)μ)1/n.

In every degree the length can be chosen less than (5/2)μ1/n.

Scaling implication. For n≥3, apply the preceding assertion to g(z)=s−nf(sz), where s=((25/13)μ)1/n. Its least critical-value modulus is 13/25, and rescaling its connection gives the first bound. The estimate 2(25/13)1/n<5/2 holds for n≥3. For n=2, write f(z)=(z−h)2−d2 and use the root segment, of length 2|d|=2μ, contained in Kμ(f). ◻

The analytic argument

Assume that no pair has a connection of length less than 2 in Ωf. At a regular level t∈(μ,1), let Ct contain a chosen first merger and let k≥2 be its root count. Put a=Area⁡(Ct)/π and x=log⁡(t/μ); Pólya’s inequality gives a≤1 [7]. Uniformise Ct by the disc, with d(0,s)=2artanh⁡s for 0≤s<1. For roots at hyperbolic distance d, choose φ:D→Ct sending ±s to them. Then d=4artanh⁡s and ∫D|φ′|2dA=πa. Cauchy–Schwarz with the Bergman kernel gives

length⁡(φ([−s,s]))2≤a∫−ss∫−ssdudv(1−uv)2=2alog⁡cosh⁡(d/2).

Thus pairwise root distances are at least D, where cosh⁡(D/2)=e2/a.

To control the distances from the centre as well, choose a point h on a connected set through the first pair in Kμ(f) whose intrinsic distance from every root is at least 1. Here intrinsic distance means the infimum of Euclidean curve lengths in Ct. Such an h exists: the intrinsic open unit balls about distinct roots are disjoint, since an intersection would give a path shorter than 2, and disjoint open sets cannot cover a connected set containing two roots. Choose the uniformisation to send 0 to h. If dj are the resulting hyperbolic root distances from 0, then

λ(dj)≤12δ(a),∑jλ(dj)≥x,λ(d)=−log⁡tanh⁡(d/2),δ(a)=−log⁡(1−e−1/a).

The one-root Bergman estimate gives the first bound because every root has intrinsic distance at least 1 from h. For the second, the component-wise Blaschke representation [8] expresses f/t in disc coordinates. Since h is not a root and lies in Kμ(f), evaluation at 0 gives ∑jλ(dj)=log⁡(t/|f(h)|)≥x. Dividing the required sum x by the maximum contribution δ(a)/2 gives k≥2x/δ(a). This uses only distances from the centre. To exploit the pairwise separation too, we intersect the disjoint hyperbolic balls about the roots with a common circle. The passage through a first merger, including simultaneous mergers, is part of the analytic input still to be formalised.

On a fixed hyperbolic circle of radius r>0 centred at 0, the balls of radius D/2 cut out disjoint arcs. Their angular half-widths satisfy

w(d,r)=arccos(clamp[−1,1]⁡cosh⁡dcosh⁡r−cosh⁡(D/2)sinh⁡dsinh⁡r),∑jw(dj,r)≤π.

Here clamp[−1,1] truncates to [−1,1]. This circle-slice inequality is formalised separately. To turn it into a root count, majorise the contribution of one root by weighted slice widths: choose σi≥0, ri>0 and U>0 such that λ(d)≤U+∑iσiw(d,ri) whenever d>0 and λ(d)≤δ(a)/2. Summing at the roots and using the angular bound at each ri gives

(5)k≥x−π∑iσiU.

The circle must be fixed before taking these intersections: angular projections of disjoint balls at different distances can overlap.

We now convert the root count into area growth. Lift one common value radius from all k roots to ∂Ct and join successive endpoints by boundary arcs. All pieces stay in Ωf because t<1. Splitting the lift integral at level μ bounds the mean total lift length by ka(x+2)/2. Each of the k resulting root-to-root connections has length at least 2; their sum counts each lift twice and the boundary once. Hence 2k≤2ka(x+2)+H1(∂Ct). Combining this with H1(∂Ct)2≤2πkt(d/dt)Area⁡(Ct) yields the ordinary differential inequality

(6)a′(x)≥12π2[2k−2a(x)(x+2)]+2.

Here the derivative is with respect to x, between merger levels. The companion proves the lift estimate and accounts for the nonnegative area jumps at mergers; those jumps do not weaken the lower bound.

The recorded rational comparison

At each level use the largest integer lower bound for the current root count k: (5), k≥2x/δ(a), or the companion’s two further packing estimates. The starting bound a(3/105)>10−6 follows by integrating (6) with k≥2 and a≤1; it is not an extra assumption on the polynomial. The recorded rational calculation then reaches a>1 by

X=6357628895991012.

It used 18 area levels, 126 certified weighted inequalities and a maximum step 1/400. On each interval [u,v] of possible root distances, the calculation bounds λ(d)−∑iσiw(d,ri) by λ(u)−∑iσimin(w(u,ri),w(v,ri)); on the tail, λ itself suffices. Thus numerical optimisation only proposes the weights. Rational inequalities certify a valid U on the whole admissible half-line, as required by (5). The endpoint minimum is valid because each slice width, as a function of d, increases and then decreases, or is monotone; it has no interior dip. This is an interval bound, not sampling between grid points.

Since t=μex, the contradiction a>1 occurs before level 1 provided that μeX<1. The recorded comparison gives (13/25)eX<0.982000386<1. It also gives (529/1000)eX<0.998996547, so the ordinary argument supports that sharper threshold as well. Neither threshold is claimed optimal, and this arithmetic does not formalise the analytic reduction.

A related ordinary averaging argument, also unformalised in its analytic construction, gives the following bounds. For a monic polynomial of degree n≥2, two zero occurrences can be joined in K2μ(f) with length at most (71/10)μ1/n; they are distinct in the squarefree case, and a repeated root gives a constant path. When μ≤1/2, the argument gives a path of length at most 5.7 in Ωf. The proof, together with refinements that retain the number of zeros in the component or its logarithmic capacity, is given in the inverse-ray averaging argument.

An isolated simple critical value

Smallness of the least critical value is not the only useful condition. An isolated simple critical value lets us continue the two branches meeting there without encountering further branching. After dividing values by v=f(c)≠0, the critical value is 1 and the roots lie over 0. We seek a disc containing both points but no other critical value. Its centre w0∈[0,1] and radius S must therefore satisfy S>max(w0,1−w0).

The ordinary construction combines a square-root coordinate, a Bergman length estimate and a component-area bound. These are the contents of the unformalised input DiscSepBergmanArea; the formal consequences below remain conditional on it.

Remark 5.1 (unformalised isolated-value assertion). Let f be monic of degree n≥3, let c be a simple critical point, and put v=f(c)≠0. Fix w0∈[0,1] and S>max(w0,1−w0). Suppose every other critical point d satisfies

|f(d)v−w0|≥S.

Put p=w0(1−w0). Then two distinct roots are joined inside {|f|≤|v|} by a curve Γ satisfying

(7)length⁡(Γ)2≤2|v|2/n(Sn−1)2/nlogS2+S+pS2−S+p.

For example, f(z)=z3−3a2z with 0<a<1/3 has zeros 0,±3a. At c=a its critical value is v=−2a3 and the other normalised critical value is −1. Thus the disc with centre w0=1 and radius 4/3 satisfies the separation hypothesis.

Remark 5.2 (conditional numerical thresholds). Let f be monic of degree n≥3 with all roots in the open unit disc. If c is a simple critical point with 0<|f(c)|<1 and, for some w0∈[0,1], every other critical point d satisfies

|f(d)f(c)−w0|≥43,

then two roots are joined inside {|f|<1} by a curve of length strictly below 2. In degree three the branch-centred choice w0=1 already works with 4/3 replaced by 6/5.

Square roots and component area

The ordinary argument first removes the scale of v, then constructs a curve, and finally bounds its length. Choose αn=v and set P(z)=v−1f(c+αz). This polynomial is monic, with its chosen critical point at 0 and critical value 1; Euclidean lengths are multiplied by |α|=|v|1/n on returning to the original plane. The component U of P−1(D(w0,S)) containing 0 has degree two. To apply Riemann–Hurwitz, exhaust it by components above regular inner discs: the outer boundary itself may contain other critical values. Since U is simply connected and 1−P has only a double zero at 0 there, it has a single-valued analytic square root ξ. This square root removes the simple branching. It is a proper local biholomorphism onto V={ξ:|ξ2−(1−w0)|<S}, a star-shaped and hence simply connected domain. Thus it is biholomorphic. Its inverse maps −1 and 1 to the two roots and [−1,1] to their connection. Along this interval P=1−ξ2∈[0,1], which gives the required containment. Let L be the Euclidean length of this normalised curve.

Put a=1−w0 and p=w0(1−w0). Squaring maps V onto D(a,S). A Möbius map from this disc to the unit disc fixing 0, followed by taking a square root, gives the conformal map

ζ=ξSS2+aξ2−a2.

Choose the square-root factor positive at 0. The endpoints ξ=±1 then map to ζ=±q, where q2=S/(S2+p). The hypothesis on S gives S2−S+p=(S−w0)(S−(1−w0))>0, so 0<q<1. The Bergman segment estimate used in Section 4 now applies to [−q,q] and gives

L2≤2πlog⁡S2+S+pS2−S+pArea⁡(U).

The factor n−1 comes from the roots outside U, not from Pólya’s inequality alone. For monic F of degree n and regular level t>0, let W be a component of {|F|<t} containing k<n zeros counted with multiplicity. Reflecting the n−k exterior-root factors into the disc gives a Blaschke product B of degree n−k with |B(0)|=cap⁡(W―)n/t and |B′|<n on the boundary. The boundary-fibre identity gives

n−kn<∑B(ζ)=w|ζ|=11|B′(ζ)|=1−|B(0)|2|w−B(0)|2,|w|=1.

Choosing w opposite B(0) gives (n−k)/n<(1−|B(0)|)/(1+|B(0)|), hence cap⁡(W―)n/t<k/(2n−k).

Apply this to F=P−w0 on the regular inner components exhausting U. Their degree is two, so k=2 and k/(2n−k)=1/(n−1). Here k counts preimages of w0 under P. These need not be the roots joined by the curve; the component degree gives both counts. Pólya’s area–capacity inequality [15], [7], followed by exhaustion, now gives Area⁡(U)≤π(S/(n−1))2/n. The original curve has length length⁡(Γ)=|v|1/nL, which gives (7). Dubinin’s relative area inequality [14] has a different full-covering hypothesis; the absolute component estimate is needed here.

For the conditional threshold, decrease S to 4/3. Since p≥0 and n≥3, the logarithm is at most log⁡7<2 and (S/(n−1))2/n≤1, giving length⁡(Γ)<2|v|1/n<2. For n=3,w0=1,S=6/5, use (3/5)2/3log⁡11<2. The chosen critical value must be nonzero and have modulus less than one. Root locations by themselves do not isolate it from the others.

Further estimates

Root distances do not ensure containment

Order the root distances at a non-root critical point c as 0<d1≤⋯≤dn. The balance ∑j(c−zj)−1=0 and this ordering give

1d1≤n−1d2,d1d2n−1≤|f(c)|.

The ratio bound 1≤d2/d1≤n−1 permits the scalar comparison

d1+d2≤2(d1d2n−1)1/n≤2|f(c)|1/n.

Neither inequality supplies containment.

When all zeros lie in the open unit disc, a different estimate holds: at every non-root critical point the sum of the distances to the two nearest zeros is strictly less than 2. The companion gives both root-distance estimates. The nearest pair is chosen among all roots of f. It need not be the pair in the two-root component of the degree-seven example, where containment restricts which pair can be joined.

Even a short segment from a critical point can leave the lemniscate. For the quintic

(z−a)(z2+p2)(z2+902901pz+p2),p=9991000,a=901902p,

all roots lie in the disc and 0 is a non-root critical point, but its unique nearest-root segment leaves the unit lemniscate. Moreover, every root-pair midpoint of z3−(99/100)3 lies outside it. This cubic still admits the two-segment connections of Theorem 3.1; it is the straight chords that fail. The exact counterexamples include the escape calculations.

Nor do the two critical-value criteria cover every polynomial in the root-disc class. For z3+3z/100−3/4, the least critical-value modulus exceeds 13/25, and the two normalised critical values are too close for the isolation criterion.

A further cubic has two roots at its first merger but normalised component capacity one at level 2μ. By that level all three roots have merged, so the initial two-root count cannot be used at the later level. The component is now the whole filled lemniscate, whose capacity is given by cap⁡(Kt(f))=t1/n [23].

Finally, z8−(3/2)z has least critical-value modulus μ>1, yet a one-root unit-level component has perimeter larger than Γ(1/4)2/(2π); see the companion’s component examples. No root-location restriction is imposed. The open question asks for a constant β bounding each component perimeter of Kσ(f) by βσ1/n, uniformly over squarefree monic f of degree n≥2 and 0<σ<μ. This level restriction is stronger than a one-root condition on a single component. Although [21] reports a Runge construction of unbounded one-root perimeters, its proof is unavailable and we do not use it.

Sparse families and binomial chords

Let f(z)=P((z−h)q), where q≥2 and P is a monic cubic, and suppose all zeros of f lie in the open unit disc. For any root r=yq of P, averaging |h+yζ|2 over the qth roots of unity cancels the cross term and gives |h|2+|y|2<1. Thus the quotient roots satisfy |r|=|y|q<1. If f has two distinct zeros, the companion selects a nonzero root r with [0,r]⊂{|P|<1}. Choose yq=r. Then f(h+tyζ)=P(tqr) for 0≤t≤1, so the whole fibre gives contained segments through h. Two distinct fibre points are joined with length 2|y|<2, using the same average.

For f(z)=z5+az4+bz+c with open-disc roots, Abel summation gives a contained radial segment whenever |bzj+c|<1. For a≠0, the missing coefficients fix the first three power sums. After rotation, the companion’s harmonic function sums to 5−2|a| over the roots. It is bounded above by 4−2|a| on the disc and by 2/31 at roots with |bzj+c|≥1. Four such indices would therefore give

5−2|a|≤4−2|a|+831<5−2|a|,

a contradiction. Hence two indices satisfy |bzj+c|<1. When a=0, the root equation gives |bzj+c|=|zj|5<1 directly. Coincident selected root values give the constant path. The companion gives the cubic-fibre proof and the quintic selection argument, including repeated root occurrences.

For zn−rn, 0<r<1, the maximum modulus on an adjacent chord of radius 0<s≤r is rn+(scos⁡(π/n))n. The outer root chord therefore works below r∗=(1+cosn⁡(π/n))−1/n. At and above this value, take a slightly contracted inner radius s>0 making that maximum less than one. The radial legs remain contained, and for n≥3 the total length is

2(r−s)+2ssin⁡(π/n)<2r<2.

The chord calculation proves the maximum on the entire segment, not geodesic optimality. For n=2, use the diameter.

Collinear roots

For collinear roots of diameter D, a Chebyshev alternation argument gives two adjacent root occurrences whose segment satisfies

|f|≤(D/2)n2n−1cosn⁡(π/(2n)).

The constant is sharp, with equality for the appropriately scaled zeros of the Chebyshev polynomial Tn. Qualitative existence of a contained root segment was already proved in [2]. For distinct roots, first reduce to the real monic case. If every gap maximum exceeded the bound, subtracting the endpoint-normalised monic Chebyshev polynomial would give a polynomial of degree at most n−1 with n distinct zeros: two endpoints and n−2 intervening sign changes. See Eremenko and Yuditskii [10] for the critical-sequence viewpoint. The companion contains the alternation proof and equality case.

Critical-value means

For cj∈D― and positive weights of sum one, set G(z)=∏j|1−c¯jz|wj. Then ∑jwjG(cj)2≤1, with equality only when all cj=0.

For interior centres, the nonvanishing factors give an analytic g(z)=1+∑ν≥1aνzν with |g|=G. On ζ=eiθ the weighted Poisson kernel is P=∑jwj(1−|cj|2)/|ζ−cj|2=1−2Re⁡(ζg′/g). With dm=dθ/(2π), subharmonicity gives the inequality below, and orthogonality gives the identity:

∑jwjG(cj)2≤∫|g|2Pdm=1−∑ν≥1(2ν−1)|aν|2.

Indeed, ∫|g|2dm=1+∑|aν|2 and ∫ζg′g―dm=∑ν|aν|2. Each nonconstant coefficient therefore contributes 1−2ν<0. For boundary centres, replace cj by rcj and let r↑1 with a finite coefficient sum first; no boundary logarithm is needed. Equality forces every aν to vanish. Logarithmic differentiation of g=1, grouping repeated centres, then forces all the positive-weight centres to be zero.

To apply this inequality to a monic polynomial f of degree n≥2 with zeros in the closed unit disc, take its m=n−1 critical points, counted with multiplicity, and give them equal weights 1/m. Gauss–Lucas puts these points in the closed unit disc. The reflected-derivative comparison then gives the pointwise bound

|f(cj)|2/m≤(∏k=1m|1−c¯kcj|)2/m=G(cj)2.

Summing and using the weighted inequality gives ∑j|f(cj)|2/m≤m. For zeros in a closed disc with centre h and radius R>0, apply this to R−nf(h+Rz) and scale back to obtain ∑j=1n−1|f(cj)|2/(n−1)≤(n−1)R2n/(n−1). If R=0, all critical values vanish. An unformalised refinement, recorded as an ordinary argument, uses g2 in the same Poisson integral and gives the proposed fourth-power bound

∑j=1n−1|f(cj)|4/(n−1)≤(n−1)R4n/(n−1)

for the same enclosing disc. Equality is attained by (z−h)n−λ with |λ|=Rn. The companion supplies the weighted identity, reflected-derivative comparison and equality analysis.

Applying AM–GM to ∑j|f(cj)|2/(n−1)≤n−1 in the unit disc gives Dubinin’s sharp critical-value product bound [16]. With a zero prescribed at the disc centre, his Theorem 3 gives a different, sharper product estimate and credits earlier work of Tischler [20]. The corresponding marked-zero positive-moment question in [21] remains unresolved here. To turn any of these mean bounds into a short-path theorem, one would still have to select a pair of roots and control a curve joining them inside the lemniscate.

Successive merger scales

For a component with k≥1 roots, let r∈(0,1] be the earlier merger level divided by the later one. An integral arising in length estimates is

Ik(r)=∫r1dqqlog⁡((1+q2/k)/(1−q2/k))=kΦ(1klog⁡1r),Φ(x)=∫0xdtlog⁡coth⁡t.

Substituting q=e−kt gives the identity; the integrand defining Φ has limiting value zero at t=0. It is increasing, so Φ is strictly convex and Φ(x)/x→0 as x↓0. Thus, when the two merger levels approach one another (r↑1), Ik(r) becomes arbitrarily small relative to k−1log⁡(1/r), even for fixed k. No positive uniform lower factor exists. See the merger-scale calculation.

Flow constructions and remaining questions

Inverse rays and perturbation

Along an existing real-interval trajectory z˙=−f(z)/f′(z) with f′(z(t))≠0, the chain rule gives (f∘z)′=−f∘z, hence f(z(t))=e−(t−t0)f(z(t0)). This classical identity fixes the ray of a nonzero value, not the Euclidean length ∫|f(z(t))/f′(z(t))|dt; see Kozen and Stefánsson [6] on the Newtonian graph of Shub, Tischler and Williams. The companion’s local complex-parameter identities for (f∘z)′ and (etf(z(t)))′ are pointwise statements, distinct from the real-interval integration in its value and finite-endpoint theorems.

For a finite interval [a,b], assume the Newton equation only for a<t<b and continuity of f(z(t)) up to both endpoints. The interior identity then extends to f(z(b))=ea−bf(z(a)), without evaluating f/f′ at an endpoint. Nonzero endpoint values therefore lie on the same positive ray. Critical values with distinct arguments exclude such a connection; distinct moduli are insufficient.

Adding β leaves f′ unchanged and sends each critical value v to v+β. For distinct values a,b, a common positive ray requires β to lie on the real line through −a and −b. Avoiding these finitely many lines and the points −v therefore makes the distinct values nonzero and ray-separated; equal values remain equal. The formal sources give the one-parameter collision locus and the finite affine-line avoidance argument. The companion calculation describes the forbidden translations; its unformalised linear-perturbation argument supplies distinct critical values. Neither qualitative step controls the slack in a near-extremal path inequality. Separately, expand log⁡|f| about a non-root point and let q be the displacement divided by the distance to the nearest zero. For q<1, the remainder after order N is at most nqN+1/((N+1)(1−q)). This local expansion cannot be used through a zero and does not itself give a coefficient-perturbation bound.

Inverse-branch prerequisites.

For a nonconstant complex polynomial, each component of {|f|<1} contains a root. The restriction to that component is onto the unit disc and has finite fibres. Over values avoiding the critical values attained in that component, it is a covering map. When 0 is not a critical value on the component, choose finitely many nonzero slit starts including its critical values, and remove their outward rays from the value disc. On the remaining domain, each root in the component determines a unique continuous inverse branch, taking 0 to that root. The archived Lean source states these prerequisites and supplies proof scripts; a kernel-check receipt for this module is not supplied here. The full conformal sheet decomposition, sheet count, monodromy and embedded-tree assertions remain ordinary arguments in the companion; the prerequisites give no length estimate.

The failed tree estimate

For z2−(9/10)2, the distance between the roots already forces any connected set containing them to have length at least 9/5. Proposition 12 of the March manuscript [3] instead proposes a bound below 41/25 plus an arbitrarily small error. Since 41/25<9/5, choosing the error smaller than this gap contradicts the lower bound. The spanning-tree estimate is false. At a simple saddle the local level set has four sectors, consistently with the lemniscate graph description in [13]. The Cassini calculation and corrected topological statement separate the metric failure from the valid sheet decomposition.

The full topological reconstruction in that discussion remains unformalised. Cutting outward from critical values to obtain inverse-sheet adjacency is classical; see [16] and [22]. Length control requires additional estimates on the actual pieces and their attachment. An uncut Newton orbit space can even fail to be Hausdorff, so it cannot be identified with a finite Reeb graph without further argument. Earlier grid searches in degrees 5,6,8,10 found no counterexample, but neither certified containment along unexamined edges nor established a statement for all polynomials.

Restricted extremal problems

The companion records the following ordinary compactness argument, which has not been formalised. In the closed lemniscate K1(f), a finite infimum of connecting path lengths is attained. At fixed degree, compactness of the closed root-disc class and lower semicontinuity of this infimum allow uniform upper bounds to pass to coefficient limits. These are statements about the closed lemniscate, as proved in the companion’s compactness argument. Closed containment survives such limits; strict containment need not. The binomial family approaches length 2, but the degree-seven example rules out 2 as a universal upper bound. That refuted assertion is not a remaining open problem. What remains is to determine quantitative bounds for restricted classes and as the degree varies.

The precise unresolved questions about cut-open flow strips, attachment lengths and quantitative perturbation are stated in the companion’s final questions. The origin-spoke failure for the near-regular-pentagon family has an ordinary, unformalised proof there. The stronger failure asserted in the research addendum [21] for every critical joining point has no available proof and is not used. Likewise the fixed degree-seven proof does not establish the whole small-parameter family.

Related results and verification

Several nearby results concern different geometric quantities. Inverse branches, slit domains and capacity also occur in Crane’s work on Smale’s mean-value conjecture [17], but its derivative normalisation differs from the monic normalisation used here. Eremenko and Hayman’s bound H1{|p|=1}<9.173deg⁡p [9] concerns total boundary length, not an internal root-to-root path. Their connectedness result, the derivative estimate of Eremenko and Lempert [11], and its equality analysis [12] likewise concern different extremal quantities. Kuznetsova and Tkachev [19] study length functions on regular levels; log-convexity there does not give a uniform one-root perimeter bound at a critical endpoint.

The hypotheses and endpoints also matter. Dubinin’s four-point distortion theorem [18] assumes a bound on all critical values, with a different normalisation. Pendyala’s Problem 1120 result [5] joins 0 to the unit circle inside a lemniscate intersected with the closed disc. Neither the endpoints nor that region restriction are those of Problem 1041.

Verification and reproducibility.

The supplied Lean sources prove the fixed counterexample for preconnected sets, the negation and answer(False) forms of the Formal Conjectures statement, and the total-variation formulation. They also prove the trinomial theorem and the other formally supported estimates identified in the companion’s verification notes. No fresh Lean build or independent human review is reported here, including review of the correspondence with the 1958 wording. The recorded full rational replay on 29 September 2026 reproduced the stopping time and 126 dual certificates; those are the computational results cited here. The analytic assertions in Remarks 4.1–5.2, the fourth-power mean and the later topological and compactness arguments remain outside the formal conclusions. The evidence record retains the statement identifiers and their conditional dependencies.

References

  1. T. F. Bloom, Erdős Problems, problem 1041. https://www.erdosproblems.com/1041

  2. P. Erdős, F. Herzog, and G. Piranian, Metric properties of polynomials, J. Analyse Math. 6 (1958), 125–148, doi:10.1007/BF02790232.

  3. shtuka, A Short Path Joining Two Zeros Inside a Polynomial Lemniscate, manuscript posted 24 March 2026, 48 pp. https://shtuka123.github.io/1041/main.pdf

  4. V. S. Pendyala, A Degree-Four Lemniscate Path Theorem, arXiv:2606.24875v1 (2026), doi:10.48550/arXiv.2606.24875.

  5. V. S. Pendyala, Shortest paths in polynomial lemniscate sublevel sets and a problem of Erdős, arXiv:2606.19178v1 (2026), doi:10.48550/arXiv.2606.19178.

  6. D. Kozen and K. Stefánsson, Computing the Newtonian graph, J. Symbolic Comput. 24 (1997), no. 2, 125–136, doi:10.1006/jsco.1997.0118; authors’ copy https://www.cs.cornell.edu/kozen/Papers/newton.pdf.

  7. E. Crane, The areas of polynomial images and pre-images, Bull. London Math. Soc. 36 (2004), no. 6, 786–792, doi:10.1112/S0024609304003509; preprint arXiv:math/0302189v1, whose statement numbers are cited.

  8. P. Ebenfelt, D. Khavinson, and H. S. Shapiro, Two-dimensional shapes and lemniscates, in Complex Analysis and Dynamical Systems IV, Part 1, Contemp. Math. 553, Amer. Math. Soc., Providence, RI, 2011, 45–59, doi:10.1090/conm/553/10931; preprint arXiv:1003.4567v1, whose statement numbers are cited.

  9. A. Eremenko and W. Hayman, On the length of lemniscates, Michigan Math. J. 46 (1999), no. 2, 409–415, doi:10.1307/mmj/1030132418; preprint arXiv:0805.2295.

  10. A. Eremenko and P. Yuditskii, Comb functions, Contemp. Math. 578 (2012), 99–118, doi:10.1090/conm/578/11472; preprint arXiv:1109.1464v1.

  11. A. Eremenko and L. Lempert, An extremal problem for polynomials, Proc. Amer. Math. Soc. 122 (1994), no. 1, 191–193, doi:10.1090/S0002-9939-1994-1207536-1.

  12. A. Eremenko, A Markov-type inequality for arbitrary plane continua, Proc. Amer. Math. Soc. 135 (2007), no. 5, 1505–1510, doi:10.1090/S0002-9939-06-08640-0; preprint arXiv:math/0606745v1.

  13. C. J. Bishop, A. Eremenko, and K. Lazebnik, On the shapes of rational lemniscates, Geom. Funct. Anal. 35 (2025), no. 2, 359–407, doi:10.1007/s00039-025-00704-2; preprint arXiv:2407.14610v1.

  14. V. N. Dubinin, Some inequalities for polynomials and rational functions associated with lemniscates, Zap. Nauchn. Sem. POMI 404 (2012), 83–99; English translation, J. Math. Sci. 193 (2013), no. 1, 45–54, doi:10.1007/s10958-013-1432-4.

  15. G. Pólya, Beitrag zur Verallgemeinerung des Verzerrungssatzes auf mehrfach zusammenhängende Gebiete, Sitzungsberichte der Preussischen Akademie der Wissenschaften, Physikalisch-Mathematische Klasse (1928), printed pp. 228–232 and 280–282. https://archive.org/details/sitzungsbericht1928preu.

  16. V. N. Dubinin, Inequalities for critical values of polynomials, Sb. Math. 197 (2006), no. 8, 1167–1176, doi:10.1070/SM2006v197n08ABEH003793.

  17. E. Crane, A bound for Smale’s mean value conjecture for complex polynomials, Bull. London Math. Soc. 39 (2007), no. 5, 781–791, doi:10.1112/blms/bdm063; author preprint https://people.maths.bris.ac.uk/~maetc/SMVCbound.pdf.

  18. V. N. Dubinin, Four-point distortion theorem for complex polynomials, arXiv:1301.3985v1 (2013).

  19. O. S. Kuznetsova and V. G. Tkachev, Length functions of lemniscates, Manuscripta Math. 112 (2003), 519–538, doi:10.1007/s00229-003-0411-3; preprint arXiv:math/0306327.

  20. D. Tischler, Critical points and values of complex polynomials, J. Complexity 5 (1989), no. 4, 438–456.

  21. W. Cook / Plectis, Three refinements for the lemniscate-path programme, 16 September 2026, unreviewed research note, Sections 1–3, together with the earlier note Structural obstructions.

  22. V. N. Dubinin, Lemniscates and inequalities for the logarithmic capacities of continua, Mat. Zametki 80 (2006), no. 1, 33–37; English translation, Math. Notes 80 (2006), no. 1, 31–35, doi:10.1007/s11006-006-0105-8.

  23. T. Ransford, Potential Theory in the Complex Plane, London Mathematical Society Student Texts 28, Cambridge University Press, Cambridge, 1995, doi:10.1017/CBO9780511623776.

PDF and source links follow the latest files on GitHub. The web reader shows the edition published here.

Lean source files

134 source files, each a programme or result file. See them in the Lean map.

The programme directory, linked result sources and their local imports. Shared files can appear in more than one programme.

  • GitHub lean/ErdosProblems/Erdos1041/AbelControlPolygon.lean
  • GitHub lean/ErdosProblems/Erdos1041/AttachmentAwareReeb.lean
  • GitHub lean/ErdosProblems/Erdos1041/CircleSeriesTransport.lean
  • GitHub lean/ErdosProblems/Erdos1041/ConnectorR18/All.lean
  • GitHub lean/ErdosProblems/Erdos1041/ConnectorR18/Averaging.lean
  • GitHub lean/ErdosProblems/Erdos1041/ConnectorR18/CollectiveReduction.lean
  • GitHub lean/ErdosProblems/Erdos1041/ConnectorR18/CubicBranch.lean
  • GitHub lean/ErdosProblems/Erdos1041/ConnectorR18/CurveAlgebra.lean
  • GitHub lean/ErdosProblems/Erdos1041/ConnectorR18/FiniteAssembly.lean
  • GitHub lean/ErdosProblems/Erdos1041/ConnectorR18/NumericalBounds.lean
  • GitHub lean/ErdosProblems/Erdos1041/ConnectorR18/PolynomialBranches.lean
  • GitHub lean/ErdosProblems/Erdos1041/ConnectorR18/R13Relevance.lean
  • GitHub lean/ErdosProblems/Erdos1041/ConnectorR18/SupplierReduction.lean
  • GitHub lean/ErdosProblems/Erdos1041/Counterexample/Algebra.lean
  • GitHub lean/ErdosProblems/Erdos1041/Counterexample/Assembly.lean
  • GitHub lean/ErdosProblems/Erdos1041/Counterexample/BarrierAlgebra.lean
  • GitHub lean/ErdosProblems/Erdos1041/Counterexample/BarrierCertificates.lean
  • GitHub lean/ErdosProblems/Erdos1041/Counterexample/BarrierGraphs.lean
  • GitHub lean/ErdosProblems/Erdos1041/Counterexample/BarrierSigns.lean
  • GitHub lean/ErdosProblems/Erdos1041/Counterexample/Bottleneck.lean
  • GitHub lean/ErdosProblems/Erdos1041/Counterexample/CatalogueAdapter.lean
  • GitHub lean/ErdosProblems/Erdos1041/Counterexample/Components.lean
  • GitHub lean/ErdosProblems/Erdos1041/Counterexample/Defs.lean
  • GitHub lean/ErdosProblems/Erdos1041/Counterexample/HausdorffLength.lean
  • GitHub lean/ErdosProblems/Erdos1041/Counterexample/InstanceBarriers.lean
  • GitHub lean/ErdosProblems/Erdos1041/Counterexample/InstanceConnectivity.lean
  • GitHub lean/ErdosProblems/Erdos1041/Counterexample/InstanceCritical.lean
  • GitHub lean/ErdosProblems/Erdos1041/CriticalTwoRootProximity.lean
  • GitHub lean/ErdosProblems/Erdos1041/CubicCriticalHub.lean
  • GitHub lean/ErdosProblems/Erdos1041/CubicQuotientFiberCase.lean
  • GitHub lean/ErdosProblems/Erdos1041/CyclicFiberMeanSquare.lean
  • GitHub lean/ErdosProblems/Erdos1041/CyclicTetranomialCoefficientCase.lean
  • GitHub lean/ErdosProblems/Erdos1041/CyclicTrinomialFiberCase.lean
  • GitHub lean/ErdosProblems/Erdos1041/ExponentialRemainderBound.lean
  • GitHub lean/ErdosProblems/Erdos1041/FreePointCentralCompletion.lean
  • GitHub lean/ErdosProblems/Erdos1041/FreePointHilbertCertificate.lean
  • GitHub lean/ErdosProblems/Erdos1041/FreePointTorusPshReduction.lean
  • GitHub lean/ErdosProblems/Erdos1041/FreePointUniformRadius.lean
  • GitHub lean/ErdosProblems/Erdos1041/GroupedPoleNearZero.lean
  • GitHub lean/ErdosProblems/Erdos1041/GroupedPolePolynomial.lean
  • GitHub lean/ErdosProblems/Erdos1041/LogKernelCentralCertificate.lean
  • GitHub lean/ErdosProblems/Erdos1041/LogKernelEnergy.lean
  • GitHub lean/ErdosProblems/Erdos1041/LogKernelVariance.lean
  • GitHub lean/ErdosProblems/Erdos1041/NewtonFlowRaySeparation.lean
  • GitHub lean/ErdosProblems/Erdos1041/NewtonFlowTrajectory.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperAnalyticTargets.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR20/CriticalMeanWhole.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR20/NewtonRealTime.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR20/SexticSpokeWhole.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR20/TwoNearestPolynomial.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR20/TwoNearestWhole.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/ArityNotCapacity.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/BinomialChords.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/CollinearDiameterWhole.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/ConstantFactorAreaCriteria.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/CriticalValueSeparationTransport.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/DiskFamilySeparationThreshold.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/GammaQuarterBound.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/HyperbolicCirclePacking.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/HyperbolicLawOfCosines.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/InverseSheetRayKernels.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/LobeAndArity.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/LobeUnconditional.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/LowCriticalScaleTransport.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/MergerScaleOrlicz.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/PlanePerimeterBound.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/PrimitiveQuinticClosedDisc.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/SeparationParent.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/StoppingTimeCertificate.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCompleteR21/SubcriticalPerimeterPath.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCorrespondenceAudit.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCriticalConsequencesR10.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCriticalValueMeanR10.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCubicCompletion.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCubicFibres.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCubicSchur.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperCurveAssembly.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperMetricScaling.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperMomentConsumers.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperNewtonEndpoints.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperPrimitiveCompletionR10.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperPrimitivePath.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperReflectedBoundary.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperReflectedCompletion.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperSeparationCounterexample.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperStraightObstructions.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperTrinomial.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperTrinomialCoverageAuditR20.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperTrinomialWholeR21.lean
  • GitHub lean/ErdosProblems/Erdos1041/PaperWeightedRefinementsR10.lean
  • GitHub lean/ErdosProblems/Erdos1041/PoissonKernelBridge.lean
  • GitHub lean/ErdosProblems/Erdos1041/PoissonNormSquare.lean
  • GitHub lean/ErdosProblems/Erdos1041/PolynomialDiscNormalisationR10.lean
  • GitHub lean/ErdosProblems/Erdos1041/PrimitiveQuinticBoundaryTail.lean
  • GitHub lean/ErdosProblems/Erdos1041/PrimitiveQuinticInteriorTail.lean
  • GitHub lean/ErdosProblems/Erdos1041/ReturnV5/All.lean
  • GitHub lean/ErdosProblems/Erdos1041/ReturnV5/CrossReturnR18.lean
  • GitHub lean/ErdosProblems/Erdos1041/ReturnV5/CurveInfrastructure.lean
  • GitHub lean/ErdosProblems/Erdos1041/ReturnV5/CyclicCostSelection.lean
  • GitHub lean/ErdosProblems/Erdos1041/ReturnV5/FirstMergeReduction.lean
  • GitHub lean/ErdosProblems/Erdos1041/ReturnV5/LobeBarrier.lean
  • GitHub lean/ErdosProblems/Erdos1041/ReturnV5/NumericalEnvelopes.lean
  • GitHub lean/ErdosProblems/Erdos1041/ReturnV5/PrecriticalFinite.lean
  • GitHub lean/ErdosProblems/Erdos1041/ReturnV5/QuadraticBranch.lean
  • GitHub lean/ErdosProblems/Erdos1041/ReturnV5/RetainedEndpointAdapters.lean
  • GitHub lean/ErdosProblems/Erdos1041/ReturnV5/RootOccurrences.lean
  • GitHub lean/ErdosProblems/Erdos1041/ReturnV5/ValueSeparationGuardrail.lean
  • GitHub lean/ErdosProblems/Erdos1041/ReturnedR18V5FullAudit.lean
  • GitHub lean/ErdosProblems/Erdos1041/SeparationCounterexampleR13.lean
  • GitHub lean/ErdosProblems/Erdos1041/SharpCollinearAlternation.lean
  • GitHub lean/ErdosProblems/Erdos1041/SharpCollinearChebyshev.lean
  • GitHub lean/ErdosProblems/Erdos1041/TaylorCircleEnergy.lean
  • GitHub lean/ErdosProblems/Erdos1041/TaylorCircleIdentification.lean
  • GitHub lean/ErdosProblems/Erdos1041/TaylorCoefficientDeficit.lean
  • GitHub lean/ErdosProblems/Erdos1041/TaylorCoefficientMajorant.lean
  • GitHub lean/ErdosProblems/Erdos1041/TaylorCrossEnergy.lean
  • GitHub lean/ErdosProblems/Erdos1041/TaylorDiagonal.lean
  • GitHub lean/ErdosProblems/Erdos1041/TaylorEnergyBound.lean
  • GitHub lean/ErdosProblems/Erdos1041/TaylorFiniteDeficitR10.lean
  • GitHub lean/ErdosProblems/Erdos1041/TetranomialElementarySymmetricSelector.lean
  • GitHub lean/ErdosProblems/Erdos1041/TetranomialL2Selector.lean
  • GitHub lean/ErdosProblems/Erdos1041/TetranomialProductSensitiveSelector.lean
  • GitHub lean/ErdosProblems/Erdos1041/TetranomialTailProductSelector.lean
  • GitHub lean/ErdosProblems/Erdos1041/WeightedAnalyticEnergy.lean
  • GitHub lean/ErdosProblems/Erdos1041/WeightedAnalyticLog.lean
  • GitHub lean/ErdosProblems/Erdos1041/WeightedAnalyticModulus.lean
  • GitHub lean/ErdosProblems/Erdos1041/WeightedBoundaryDeficitR10.lean
  • GitHub lean/ErdosProblems/Erdos1041/WeightedCauchyTransportR10.lean
  • GitHub lean/ErdosProblems/Erdos1041/WeightedClosedDisc.lean
  • GitHub lean/ErdosProblems/Erdos1041/WeightedGroupedRigidityR10.lean
  • GitHub lean/ErdosProblems/Erdos1041/WeightedInteriorBound.lean
  • GitHub lean/ErdosProblems/Erdos1041/WeightedInteriorRadius.lean
  • GitHub lean/ErdosProblems/Erdos1041/WeightedPoissonIdentity.lean
  • GitHub lean/ErdosProblems/Erdos1041/WeightedRadialIdentity.lean
Statements with Lean proofs

Lean is software that verifies a formal proof against its theorem statement and assumptions. These proofs establish only the statements listed here.

  • For ani’s degree-seven polynomial, every preconnected strict-lemniscate set containing two distinct roots has one-dimensional Hausdorff measure above two. Lean refutes the exact Formal Conjectures path-image claim and checks a separate total-variation bound.
  • Along a trajectory tangent to the complex Newton vector field -f/f', the polynomial value satisfies w' =−w.
  • The exponentially rescaled polynomial value is a first integral, so the value of a Newton trajectory remains on one oriented ray.
  • A finite Newton-flow connection can only join endpoints whose polynomial values lie on the same positive ray; distinct critical-value arguments therefore exclude such a connection.
  • For two translated critical values, the ray-collision locus is a real affine line with an exact one-parameter description.
  • A finite family of ray-collision lines can be avoided by an arbitrarily small common translation.
  • An explicit root-retention estimate keeps roots of a sufficiently small constant perturbation inside the unit disc.
What these proofs do not establish
  • The full small-parameter family reported by ani; only one explicit polynomial is formalised.
  • Independent human review adjudicating whether the exact Formal Conjectures path-image-length statement represents the 1958 curve-length wording.
  • The spanning-tree decomposition claimed in the March 2026 manuscript; its printed Proposition 12 proof uses an invalid three-ended local saddle block, and a Cassini example refutes the printed global tree budget.
  • A repair of Proposition 12 that retains the printed 1/(2π) spanning-tree coefficient; any later argument must change the metric inequality.
  • A perturbation theorem that first makes critical values injective while preserving the relevant lemniscate component, collars, and strict length slack.
  • A corrected restricted-family or alternative-metric gluing theorem; universal sub-two total-variation gluing is ruled out by the degree-seven counterexample.
The formal record: 2 main results, 6 open obligations, 3 selected result modules, finite search evidence, Comparator review

Main results

Statements and their limits are copied from the public research record. Recorded status: registered_declarations

Assumptions still needing proofs

Prove any one of these and the corresponding reduction above becomes unconditional.

  • historical_curve_length_correspondence Independently review whether the 1958 curve-length wording matches the refuted Formal Conjectures path-image Hausdorff statement.
  • repair_or_refute_saddle_block Repair or replace the false Proposition 12 spanning-tree estimate; account for positive attachment costs or use another metric inequality.
  • compact_ray_cut_strip_decomposition Verify a compact ray-cut strip or cell decomposition under explicit local-valence hypotheses for restricted families; it gives no universal sub-two connector.
  • corrected_metric_gluing_for_restricted_families For a restricted family or different historical length notion, prove a metric gluing inequality that pays every positive attachment cost; universal sub-two total-variation gluing is refuted.
  • two_stage_stable_perturbation Given a selected connector with strict slack, quantify a two-stage perturbation preserving roots, component, collars, ray separation, and slack; no universal existence claim follows.
  • relative_global_newton_flow_theorem Under explicit component, saddle, and corrected metric hypotheses, derive a restricted root-to-root Newton-flow connector without a universal sub-two claim.

Selected Lean proof files

The public result record selects 3 modules. Browse all 134 source files in this programme’s source map, including shared result sources and local imported dependencies.

Comparator review

Comparator runs selected Lean proofs against separately supplied theorem statements using recorded software versions. A successful run establishes that those proofs satisfy those statements; it does not prove the unanswered questions above.

Replayed by the Comparator

Statement and type parity replayed against the pinned toolchain.

  • Collision translations are parameterised by real affine lines and an arbitrarily small common translation avoids finitely many of them.

    The finite-family avoidance theorem does not perform the global topology or metric gluing.

    translation_avoidance: targeted

  • A quantified small constant perturbation keeps every polynomial root inside the open unit disc.

    Root retention is one input to a still-incomplete route.

    root_retention: targeted

Represented indirectly

Covered through a neighbouring selected interface, not replayed one-to-one.

  • Lean checks that distinct positive rays contradict an assumed exponential endpoint relation; the paper derives that relation for a finite real-time Newton trajectory by ordinary integration and endpoint continuity.

    The finite-trajectory conclusion retains continuity on the closed interval, differentiability and noncritical Newton evolution on its interior, and the ordinary endpoint passage. It supplies neither global trajectory existence nor geometric length control.

    ray_separation: represented_by_translation_avoidance_targets

Outside the Comparator selection

Stated in the corpus; not part of the replayed interface set.

  • Lean checks the local Newton value equation and the zero-derivative form of its exponentially scaled value; constancy along a real-time interval is an ordinary calculus consequence in the paper.

    The cited declarations are pointwise derivative statements. The real-time first integral requires the paper’s interval integration step, and value decay alone does not construct a global trajectory or give a short connecting curve.

    newton_value_decay: not_selected_compact_calculus_family

  • The paper identifies an invalid local saddle block in a claimed unrestricted proof.

    The diagnosis does not prove that no repair exists.

    published_proof_gap: not_applicable_not_a_lean_proposition

  • A bounded search records finite geometric evidence.

    Finite evidence does not settle the universal problem.

    lemniscate_finite_search: not_applicable_not_a_lean_theorem

The result statements, their limits and the counts are copied from the public Lean repository’s published records identified by b0ebeb9add157584. These records are copied into the page when the website is built. Introductory explanations and labels are written for this site. The diagram at the top is the exception: a program draws it from numbers the papers print and tests the numerical relationships shown. Its caption and explanation are written for this site.