Outgoing germs after independent cuts

Each outgoing germ is multiplied by the positive width of its retained end segment. This includes one-segment routes, where the opposite cut also changes that width.

theorem Cslib.Polygonal.Route.germ_cutEnds (p : Route) (s t : ℝ) (side : Bool) : (p.cutEnds s t).germ side = (p.cutUpper t (p.endSegment side) - p.cutLower s (p.endSegment side)) • p.germ side

Independent cuts scale each outgoing germ by its retained segment width.

theorem Cslib.Polygonal.Route.arg_germ_cutEnds (p : Route) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t < 1) (side : Bool) : ((p.cutEnds s t).germ side).arg = (p.germ side).arg

Valid independent cuts preserve each literal outgoing argument.