Cutting the two ends of a finite polygonal route

Route.cutEnds moves the two listed endpoints into their original end segments and leaves all internal listed points unchanged. The two cuts are independent, including when the route has a single segment. The real local parameters are tracked explicitly, so support containment and simplicity refer to every real point of every segment.

The sum of the two cut parameters must be less than one. This suffices even for a single-segment open edge; no artificial bend or degenerate segment is introduced.

noncomputable def Cslib.Polygonal.Route.cutEnds (p : Route) (s t : ℝ) : Route

Cut the initial and final outgoing segments by parameters s and t. Internal points and their order are unchanged. Zero cuts are permitted.

def Cslib.Polygonal.Route.cutLower (p : Route) (s : ℝ) (i : Fin p.segments) : ℝ

The lower original parameter retained in a given segment after the two cuts.

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

The upper original parameter retained in a given segment after the two cuts.

noncomputable def Cslib.Polygonal.Route.cutTime (p : Route) (s t : ℝ) (i : Fin p.segments) (u : ℝ) : ℝ

The old real segment parameter of a point on the cut route.

theorem Cslib.Polygonal.Route.endpoint_cutEnds (p : Route) (s t : ℝ) (b : Bool) : (p.cutEnds s t).endpoint b = p.eval (p.endSegment b) (endTime b (if b = true then t else s))

The two new route ends are the chosen real parameters of the two old end segments.

theorem Cslib.Polygonal.Route.eval_cutEnds (p : Route) (s t : ℝ) (i : Fin p.segments) (u : ℝ) : (p.cutEnds s t).eval i u = p.eval i (p.cutTime s t i u)

Every cut segment is an affine subsegment of the original segment at the same index, including when the first and last segment are the same.

theorem Cslib.Polygonal.Route.cut_bounds (p : Route) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t < 1) (i : Fin p.segments) : 0 ≤ p.cutLower s i ∧ p.cutLower s i < p.cutUpper t i ∧ p.cutUpper t i ≤ 1

Both retained local segment endpoints lie in the old unit interval, in strict order.

theorem Cslib.Polygonal.Route.cutTime_bounds (p : Route) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t < 1) (i : Fin p.segments) {u : ℝ} (hu : u ∈ Set.Icc 0 1) : p.cutLower s i ≤ p.cutTime s t i u ∧ p.cutTime s t i u ≤ p.cutUpper t i

Every cut parameter lies between the two retained endpoints of its old segment.

theorem Cslib.Polygonal.Route.cutTime_eq_lower_iff (p : Route) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t < 1) (i : Fin p.segments) (u : ℝ) : p.cutTime s t i u = p.cutLower s i ↔ u = 0

The lower end of an affine subsegment has only the new zero parameter.

theorem Cslib.Polygonal.Route.cutTime_eq_upper_iff (p : Route) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t < 1) (i : Fin p.segments) (u : ℝ) : p.cutTime s t i u = p.cutUpper t i ↔ u = 1

The upper end of an affine subsegment has only the new unit parameter.

theorem Cslib.Polygonal.Route.cutTime_mem (p : Route) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t < 1) (i : Fin p.segments) {u : ℝ} (hu : u ∈ Set.Icc 0 1) : p.cutTime s t i u ∈ Set.Icc 0 1

Cutting both ends never sends a retained real parameter outside its old segment.

theorem Cslib.Polygonal.Route.support_cutEnds_subset (p : Route) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t < 1) : (p.cutEnds s t).support ⊆ p.support

Cutting both ends only removes actual points from the continuous support.

theorem Cslib.Polygonal.Route.atEnd_cutEnds_of_atEnd {p : Route} {s t u : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t < 1) (i : Fin p.segments) (hu : u ∈ Set.Icc 0 1) (b : Bool) (heq : p.AtEnd i (p.cutTime s t i u) b) : (p.cutEnds s t).AtEnd i u b

If a retained point was at an old route end, it is at the same end of the cut route. The converse need not hold: a positive cut creates a new end in an old segment interior.

theorem Cslib.Polygonal.Route.IsSimple.cutEnds {p : Route} (hp : p.IsSimple) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t < 1) : (p.cutEnds s t).IsSimple

Cutting the two end segments preserves continuous simplicity, also for a closed loop and for a one-segment open edge. The two cuts may have different parameters.