Prove2Me

Positive separation of a vertex from a nonincident polygonal-arc segment

Proved
PolygonalArcVertexNonincidentSegmentSeparation

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

compactnesscrossing-consequencesgeometrypolygonal

Let γ be a polygonal arc. For a listed vertex pᵢ and a listed segment [pⱼ,pⱼ₊₁] with i different from both j and j+1, there is a strictly positive number δ such that every point q on that segment remains at distance at least δ from pᵢ:

∃ δ>0such thatq∈[pj,pj+1]⟹δ≤d(pi,q).\exists\,\delta>0\quad\text{such that}\quad q\in[p_j,p_{j+1}]\Longrightarrow\delta\le d(p_i,q).

Thus a nonincident vertex and segment have a positive clearance, not merely disjoint carriers. This is the quantitative separation used to choose uniform collar-control radii around the vertices.

Preamble
import Definitions.Def_PolygonalArc
import Mathlib.Analysis.Normed.Module.Convex

open Classical
noncomputable section
Formal statement
lemma PolygonalArcVertexNonincidentSegmentSeparation (γ : PolygonalArc)
    {i j : ℕ} (hi : i < γ.vertices.length)
    (hj : j + 1 < γ.vertices.length) (hij : i ≠ j) (hijs : i ≠ j + 1) :
    ∃ δ : ℝ, 0 < δ ∧
      ∀ q, q ∈ segment ℝ γ.vertices[j] γ.vertices[j + 1] →
        δ ≤ dist γ.vertices[i] q := by sorry
Source
https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/PolygonalArcVertexNonincidentSegmentSeparation.lean#L1-L43

View graph