Adjacent polygonal-arc outward directions are not the same positive ray
ProvedPolygonalArcAdjacentOutwardDirectionsNotSameRaygeometrypolygonal-arcs
Let be a simple polygonal arc, and let be an interior vertex index. The two vectors pointing outward from the vertex along the adjacent segments cannot lie on the same positive ray, in either orientation. Equivalently, neither outward direction is a positive scalar multiple of the other.
This local nondegeneracy property prevents two consecutive segments from reversing along one line and is the geometric input needed to construct narrow endpoint and junction cones.
Preamble
import Definitions.Def_PolygonalArc open Classical noncomputable section
Formal statement
theorem PolygonalArcAdjacentOutwardDirectionsNotSameRay (γ : PolygonalArc)
{i : ℕ} (hprev : 0 < i) (hnext : i + 1 < γ.vertices.length) :
(¬ ∃ a : ℝ, 0 < a ∧
γ.vertices[i - 1] - γ.vertices[i] =
a • (γ.vertices[i + 1] - γ.vertices[i])) ∧
¬ ∃ a : ℝ, 0 < a ∧
γ.vertices[i + 1] - γ.vertices[i] =
a • (γ.vertices[i - 1] - γ.vertices[i]) := by sorrySource