Terminal ray cover near a polygonal-arc target endpoint
ProvedPolygonalArcTargetEndpointRayCovercrossing-consequencesgeometrypolygonal
For every polygonal arc , there is a positive radius such that every point of the carrier inside the target ball lies on the closed ray from the target through the penultimate vertex:
B(\gamma.target,r)\cap\gamma.carrier \subseteq \left\{\gamma.target+cigl(\gamma_{n-2}-\gamma.targetigr):c\ge0 ight\}.This identifies all arc points sufficiently close to the target with the single terminal ray that is removed from the slit disk.
Preamble
import Definitions.Def_PolygonalArc open Classical noncomputable section
Formal statement
lemma PolygonalArcTargetEndpointRayCover (γ : PolygonalArc) :
∃ r : ℝ, 0 < r ∧
(let hprev : γ.vertices.length - 2 < γ.vertices.length := by
have hlen := γ.length_ge_two
omega
Metric.ball γ.target r ∩ γ.carrier ⊆
{x | ∃ c : ℝ, 0 ≤ c ∧
x = γ.target +
c • (γ.vertices[γ.vertices.length - 2]'hprev - γ.target)}) := by sorrySource