Adding one segment to either end of a polygonal route

Route.prepend and Route.append each add exactly one real segment. Their contact conditions distinguish the two parameter ends, including when the new route closes. Adding a segment to an already closed route cannot preserve simplicity, and a new degenerate segment is rejected.

These are original finite route constructions. No topological path replacement theorem or geometric drawing provider is assumed.

def Cslib.Polygonal.Route.prepend (a : ℂ) (p : Route) : Route

Add the segment from a to the old start. This adds exactly one segment.

def Cslib.Polygonal.Route.append (p : Route) (b : ℂ) : Route

Add the segment from the old finish to b. This adds exactly one segment.

@[simp]

theorem Cslib.Polygonal.Route.segments_prepend (a : ℂ) (p : Route) : (prepend a p).segments = p.segments + 1

Prepending adds exactly one segment.

@[simp]

theorem Cslib.Polygonal.Route.segments_append (p : Route) (b : ℂ) : (p.append b).segments = p.segments + 1

Appending adds exactly one segment.

theorem Cslib.Polygonal.Route.eval_prepend_zero (a : ℂ) (p : Route) (t : ℝ) : (prepend a p).eval 0 t = (AffineMap.lineMap a p.start) t

The new initial segment has its full real affine parameter.

theorem Cslib.Polygonal.Route.eval_prepend_succ (a : ℂ) (p : Route) (i : Fin p.segments) (t : ℝ) : (prepend a p).eval i.succ t = p.eval i t

Every old segment retains its orientation and local real parameter after prepending.

theorem Cslib.Polygonal.Route.eval_append_castSucc (p : Route) (b : ℂ) (i : Fin p.segments) (t : ℝ) : (p.append b).eval i.castSucc t = p.eval i t

Every old segment retains its orientation and local real parameter after appending.

theorem Cslib.Polygonal.Route.eval_append_last (p : Route) (b : ℂ) (t : ℝ) : (p.append b).eval (Fin.last p.segments) t = (AffineMap.lineMap p.finish b) t

The new final segment has its full real affine parameter.

@[simp]

theorem Cslib.Polygonal.Route.endpoint_prepend (a : ℂ) (p : Route) (b : Bool) : (prepend a p).endpoint b = if b = true then p.finish else a

Prepending changes only the start endpoint.

@[simp]

theorem Cslib.Polygonal.Route.endpoint_append (p : Route) (b : ℂ) (side : Bool) : (p.append b).endpoint side = if side = true then b else p.start

Appending changes only the finish endpoint.

@[simp]

theorem Cslib.Polygonal.Route.germ_prepend (a : ℂ) (p : Route) (b : Bool) : (prepend a p).germ b = if b = true then p.germ true else p.start - a

The new start germ is the added segment; the old final outgoing germ is unchanged.

@[simp]

theorem Cslib.Polygonal.Route.germ_append (p : Route) (b : ℂ) (side : Bool) : (p.append b).germ side = if side = true then p.finish - b else p.germ false

The old initial germ is unchanged; the new finish germ points back along the added segment.

theorem Cslib.Polygonal.Route.position_prepend_succ (a : ℂ) (p : Route) (i : Fin p.segments) (t : ℝ) : (prepend a p).position i.succ t = 1 + p.position i t

Prepending shifts every old global route parameter by one.

theorem Cslib.Polygonal.Route.position_append_castSucc (p : Route) (b : ℂ) (i : Fin p.segments) (t : ℝ) : (p.append b).position i.castSucc t = p.position i t

Appending preserves every old global route parameter.

theorem Cslib.Polygonal.Route.IsSimple.prepend {p : Route} (hp : p.IsSimple) {a : ℂ} (ha : a ≠ p.start) (hcontact : ∀ (j : Fin p.segments) (s t : ℝ), s ∈ Set.Icc 0 1 → t ∈ Set.Icc 0 1 → (AffineMap.lineMap a p.start) s = p.eval j t → s = 1 ∧ p.AtEnd j t false ∨ s = 0 ∧ p.AtEnd j t true) : (Route.prepend a p).IsSimple

A simple route may be prepended with one nondegenerate segment if every contact is either the intended join or the two distinct parameter ends of the new closed route. The latter alternative is allowed only by actual geometric equality.

theorem Cslib.Polygonal.Route.IsSimple.append {p : Route} (hp : p.IsSimple) {b : ℂ} (hb : p.finish ≠ b) (hcontact : ∀ (i : Fin p.segments) (s t : ℝ), s ∈ Set.Icc 0 1 → t ∈ Set.Icc 0 1 → p.eval i s = (AffineMap.lineMap p.finish b) t → p.AtEnd i s true ∧ t = 0 ∨ p.AtEnd i s false ∧ t = 1) : (p.append b).IsSimple

A simple route may be appended with one nondegenerate segment under the exact parameter-level join and possible new-loop closure contact alternatives.

theorem Cslib.Polygonal.Route.IsSimple.prepend_ne {p : Route} {a : ℂ} (h : (Route.prepend a p).IsSimple) : a ≠ p.start

Simplicity rejects a degenerate newly prepended segment.

theorem Cslib.Polygonal.Route.IsSimple.append_ne {p : Route} {b : ℂ} (h : (p.append b).IsSimple) : p.finish ≠ b

Simplicity rejects a degenerate newly appended segment.

theorem Cslib.Polygonal.Route.IsSimple.prepend_start_ne_finish {p : Route} {a : ℂ} (h : (Route.prepend a p).IsSimple) : p.start ≠ p.finish

A route that was already closed cannot be extended at its start while remaining simple: its two old end occurrences would become an interior contact.

theorem Cslib.Polygonal.Route.IsSimple.append_start_ne_finish {p : Route} {b : ℂ} (h : (p.append b).IsSimple) : p.start ≠ p.finish

A route that was already closed cannot be extended at its finish while remaining simple. The old finish is an interior parameter after appending.