Parameters of routes with attached end segments

Every actual segment parameter is either an unchanged old parameter or a parameter of an attached end segment. The global position is recorded exactly, so contact proofs can recover the original route ends after one or both attachments.

theorem Cslib.Polygonal.Route.prepend_eval_cases (a : ℂ) (p : Route) (i : Fin (prepend a p).segments) (t : ℝ) : (∃ (j : Fin p.segments), (prepend a p).eval i t = p.eval j t ∧ (prepend a p).position i t = 1 + p.position j t) ∨ (prepend a p).eval i t = (AffineMap.lineMap a p.start) t ∧ (prepend a p).position i t = t

Every parameter of a prepended route is an old parameter shifted by one, or a parameter of the new initial segment. The statement holds for every real parameter.

theorem Cslib.Polygonal.Route.append_eval_cases (p : Route) (b : ℂ) (i : Fin (p.append b).segments) (t : ℝ) : (∃ (j : Fin p.segments), (p.append b).eval i t = p.eval j t ∧ (p.append b).position i t = p.position j t) ∨ (p.append b).eval i t = (AffineMap.lineMap p.finish b) t ∧ (p.append b).position i t = ↑p.segments + t

Every parameter of an appended route is an unchanged old parameter or a parameter of its new final segment, with its exact global position.

theorem Cslib.Polygonal.Route.attach_eval_cases (a : ℂ) (p : Route) (b : ℂ) (i : Fin ((prepend a p).append b).segments) (t : ℝ) : (∃ (j : Fin p.segments), ((prepend a p).append b).eval i t = p.eval j t ∧ ((prepend a p).append b).position i t = 1 + p.position j t) ∨ ((prepend a p).append b).eval i t = (AffineMap.lineMap a p.start) t ∧ ((prepend a p).append b).position i t = t ∨ ((prepend a p).append b).eval i t = (AffineMap.lineMap p.finish b) t ∧ ((prepend a p).append b).position i t = ↑p.segments + 1 + t

Attaching both ends retains every old parameter and distinguishes both new segments, even when the new route is closed.