Finite polygonal routes in the plane

A route has a positive finite number of actual straight real segments in the complex plane. Segment parameters include all real numbers in [0,1]. Simplicity identifies only adjacent segment endpoints and, for a closed route, its first and last parameter. In particular it excludes degenerate segments, retracing, tangencies and nonadjacent contacts.

This is original finite geometric infrastructure, with no numerical genus certificate or topological drawing theorem among its data or hypotheses.

Main definitions

• Cslib.Polygonal.Route: a finite nonempty chain of real planar segments.
• Cslib.Polygonal.Route.IsSimple: injectivity except for the intended endpoint closure.
• Cslib.Polygonal.Route.germ: the actual outgoing first or last segment vector.

structure Cslib.Polygonal.Route : Type

A nonempty finite segment chain. bends + 1 is its number of segments; extra collinear vertices are permitted. IsSimple allows closure only between the first and last parameters.

• bends : ℕ

  Number of internal listed points.

• point : Fin (self.bends + 2) → ℂ

  Listed points, including both ends.

@[reducible, inline]

abbrev Cslib.Polygonal.Route.segments (p : Route) : ℕ

The number of actual segments.

def Cslib.Polygonal.Route.start (p : Route) : ℂ

First listed point.

def Cslib.Polygonal.Route.finish (p : Route) : ℂ

Last listed point.

def Cslib.Polygonal.Route.endpoint (p : Route) (b : Bool) : ℂ

The endpoint selected by a dart's Boolean end tag.

noncomputable def Cslib.Polygonal.Route.eval (p : Route) (i : Fin p.segments) (t : ℝ) : ℂ

The actual i-th segment, with its full real affine parameter.

def Cslib.Polygonal.Route.position (p : Route) (i : Fin p.segments) (t : ℝ) : ℝ

The parameter on the entire chain, identifying successive segment endpoints.

def Cslib.Polygonal.Route.AtEnd (p : Route) (i : Fin p.segments) (t : ℝ) (b : Bool) : Prop

A parameter is at one of the two ends of the entire chain.

noncomputable def Cslib.Polygonal.Route.support (p : Route) : Set ℂ

All real points on all listed segments.

theorem Cslib.Polygonal.Route.at_mem_support (p : Route) (i : Fin p.segments) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : p.eval i t ∈ p.support

Every segment parameter belongs to the continuous support.

theorem Cslib.Polygonal.Route.mem_support_iff (p : Route) (z : ℂ) : z ∈ p.support ↔ ∃ (i : Fin p.segments), ∃ t ∈ Set.Icc 0 1, p.eval i t = z

Membership in the support means membership at an actual real segment parameter.

theorem Cslib.Polygonal.Route.position_mem (p : Route) (i : Fin p.segments) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : p.position i t ∈ Set.Icc 0 ↑p.segments

The chain parameter stays in its closed global interval.

theorem Cslib.Polygonal.Route.at_eq_start (p : Route) (i : Fin p.segments) {t : ℝ} (ht : t ∈ Set.Icc 0 1) (h : p.position i t = 0) : p.eval i t = p.start

At the first chain parameter the segment point is the first listed point.

theorem Cslib.Polygonal.Route.at_eq_finish (p : Route) (i : Fin p.segments) {t : ℝ} (ht : t ∈ Set.Icc 0 1) (h : p.position i t = ↑p.segments) : p.eval i t = p.finish

At the last chain parameter the segment point is the last listed point.

theorem Cslib.Polygonal.Route.at_eq_endpoint (p : Route) (i : Fin p.segments) {t : ℝ} (ht : t ∈ Set.Icc 0 1) (b : Bool) (h : p.AtEnd i t b) : p.eval i t = p.endpoint b

The point of a parameter at a selected end is that endpoint.

def Cslib.Polygonal.Route.IsSimple (p : Route) : Prop

Equal points have equal global parameters, except for the two ends of a closed route. This tests the actual continuum of each segment, not only the listed points.

theorem Cslib.Polygonal.Route.IsSimple.segment_ne {p : Route} (hp : p.IsSimple) (i : Fin p.segments) : p.point i.castSucc ≠ p.point i.succ

Every actual segment of a simple route is nondegenerate.

def Cslib.Polygonal.Route.germ (p : Route) (b : Bool) : ℂ

Outgoing vector of the first segment at the first end, or the reversed last segment at the last end. Thus loops still have two separately defined geometric germs.

theorem Cslib.Polygonal.Route.IsSimple.germ_ne_zero {p : Route} (hp : p.IsSimple) (b : Bool) : p.germ b ≠ 0

A simple route has nonzero outgoing germs at both ends.