For a monic polynomial whose roots lie in the open unit disc, must two roots be joinable by a curve of length less than two inside the open unit lemniscate?
Statements and boundaries are copied from the corpus record. Registry status: not_registered; the claim registry does not carry these declarations and kernel checking them does not promote them into reviewed public claims
An arbitrarily small common translation separates a finite injective family from zero and from shared positive rays.
Finite-family avoidance does not provide the global topological or metric gluing.
A quantified small constant perturbation keeps every polynomial root inside the open unit disc.
Root retention is only one input to an incomplete global route.
Prove any one of these and the corresponding reduction above becomes unconditional.
repair_or_refute_saddle_block Replace the false three-ended interior saddle neighbourhood by a valid four-pronged or cut-annulus block and reprove the required incidence statement, or construct a polynomial counterexample to that incidence statement.compact_ray_cut_strip_decomposition Build a compact strip or cell decomposition after cutting along critical-value rays, without presupposing the unproved local valence count.metric_gluing_below_two Glue the local pieces with strict quantitative slack while preserving the sharp one-over-two-pi length bookkeeping.two_stage_stable_perturbation First separate critical values, then apply the checked small translation, while retaining roots, the selected component, collars, ray separation, and a strict length margin.relative_global_newton_flow_theorem Prove the global relative Newton-flow theorem that turns the checked ray separation into the required root-to-root curve inside the original open lemniscate.A raster search samples named failure modes through degree ten and returns candidate upper bounds only. It is finite numerical evidence, not a topology proof or a counterexample certificate.
| Module | Lines | Declarations | Theorems |
|---|---|---|---|
ErdosProblems.Erdos1041.NewtonFlowRaySeparation |
323 | 21 | 18 |
The Comparator replays selected exact interfaces against a pinned toolchain. It never widens what Lean proved.
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
Covered through a neighbouring selected interface, not replayed one-to-one.
Distinct positive rays exclude a finite Newton connection.
The result is a route obstruction, not the global theorem.
ray_separation · represented_by_translation_avoidance_targets
Stated in the corpus; not part of the replayed interface set.
The Newton value equation and its exponential first integral are checked exactly.
Value decay alone does not 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
Newton Flow and Critical-Value Ray Separation
Along the complex Newton field, Lean checks that the polynomial value decays as exp(-t) and therefore stays on one oriented ray. It formalises the resulting no-connection criterion, the exact translation ray-collision locus, finite-line avoidance, and a root-retention bound. A recent manuscript's load-bearing Proposition 12 uses an invalid three-ended local block at an interior Morse saddle, diagnosed here independently and matching Tao's public account of the same defect; the proposition is not refuted and may admit a four-pronged or cut-annulus repair. The global topology and length gluing remain open.