Endpoint isolation radii for a polygonal arc

Proved

PolygonalArcEndpointIsolationExists

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

crossing-consequencesgeometrypolygonal

Every polygonal arc $\gamma$ admits positive radii $r_0$ and $r_1$ such that the closed endpoint balls are disjoint, each endpoint ball meets the carrier only on the corresponding first or last segment, and each radius is smaller than the length of that endpoint segment. In symbols,

\exists r_0,r_1>0,\quad \operatorname{PolygonalArcEndpointIsolation}(\gamma,r_0,r_1).

The result supplies the endpoint control data used by both the tail-source and terminal-slit-disk constructions.

Preamble

import Definitions.Def_PolygonalArcEndpointIsolation

open Classical
noncomputable section

Formal statement

lemma PolygonalArcEndpointIsolationExists (γ : PolygonalArc) :
    ∃ r₀ r₁ : ℝ, PolygonalArcEndpointIsolation γ r₀ r₁ := by sorry

Source

https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/PolygonalArcEndpointIsolationExists.lean#L1-150

View graph