Existence of collar-control radii for a polygonal arc

Proved

PolygonalArcCollarControlRadiiExists

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

crossing-consequencesgeometrypolygonal

For every polygonal arc $\gamma$ and every positive tolerance $\eta$ , there is a family of positive radii, one at each vertex, that is smaller than $\eta$ , has pairwise disjoint closed vertex balls, has adjacent radii summing to less than the corresponding edge length, and has every vertex ball disjoint from each nonincident edge. In symbols,

\eta>0\quad\Longrightarrow\quad \operatorname{Nonempty}(\operatorname{PolygonalArcCollarControlRadii}(\gamma,\eta)).

These uniform collar data are the local geometric foundation for isolating the two endpoints of a simple polygonal arc.

Preamble

import Definitions.Def_PolygonalArcCollarControlRadii

open Classical
noncomputable section

Formal statement

lemma PolygonalArcCollarControlRadiiExists (γ : PolygonalArc) {η : ℝ}
    (hη : 0 < η) :
    Nonempty (PolygonalArcCollarControlRadii γ η) := by sorry

Source

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

View graph