ArcCrossingInitialConeAvoidsBackwardGerm

Proved

ArcCrossingInitialConeAvoidsBackwardGerm

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

crossing-consequencesgeometrypolygonal

For an oriented tail whose first vertex is an interior point of a polygonal-arc edge, the initial endpoint cone is disjoint from the backward segment from that interior point to the preceding vertex. This prevents the initial cone from meeting the already traversed germ.

Preamble

import Definitions.Def_PolygonalArcInitialEndpointCone
import Definitions.Def_PolygonalArc

import Mathlib.Tactic
import Mathlib.Analysis.Normed.Affine.AddTorsor

open Classical
noncomputable section

Formal statement

lemma ArcCrossingInitialConeAvoidsBackwardGerm
    (δ τ : PolygonalArc) (j : ℕ) (c : EuclideanSpace ℝ (Fin 2))
    (r K₀ : ℝ)
    (hj : j + 1 < δ.vertices.length)
    (hcOpen : c ∈ openSegment ℝ δ.vertices[j] δ.vertices[j + 1])
    (hτvertices : τ.vertices = c :: δ.vertices.drop (j + 1))
    (hτsource : τ.source = c) :
    Disjoint (PolygonalArcInitialEndpointCone τ r K₀) (segment ℝ c δ.vertices[j]) := by sorry

Source

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

View graph