Polygonal loops above ordered ports

A loop leaves the origin towards (a,1), rises vertically, crosses horizontally at height 2 + |a-b|, returns to (b,1), and closes at the origin. Distinct disjoint or strictly nested port intervals give loops whose only common point is the origin. All statements quantify over actual real parameters of the five segments. This is an original coordinate construction.

def Cslib.Polygonal.portLoop (a b : ℝ) : Route

A five-segment closed route with ordered real ports and a horizontal upper segment. The two ports are kept in the given order, including when b < a.

@[simp]

theorem Cslib.Polygonal.endpoint_portLoop (a b : ℝ) (c : Bool) : (portLoop a b).endpoint c = 0

Both ends are the origin.

@[simp]

theorem Cslib.Polygonal.germ_portLoop (a b : ℝ) (c : Bool) : (portLoop a b).germ c = if c = true then { re := b, im := 1 } else { re := a, im := 1 }

The two actual outgoing germs point to the two separately indexed ports.

theorem Cslib.Polygonal.eval_portLoop (a b : ℝ) (i : Fin 5) (t : ℝ) : (portLoop a b).eval i t = ![{ re := t * a, im := t }, { re := a, im := 1 + t * (1 + |a - b|) }, { re := (1 - t) * a + t * b, im := 2 + |a - b| }, { re := b, im := 2 + |a - b| - t * (1 + |a - b|) }, { re := (1 - t) * b, im := 1 - t }] i

Coordinates at every real parameter on each of the five actual segments.

theorem Cslib.Polygonal.isSimple_portLoop {a b : ℝ} (hab : a ≠ b) : (portLoop a b).IsSimple

The five-segment loop is simple whenever its two ports are distinct.

theorem Cslib.Polygonal.eval_portLoop_cases (a b : ℝ) (i : Fin 5) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : have z := (portLoop a b).eval i t; z.im ∈ Set.Icc 0 1 ∧ (z.re = z.im * a ∨ z.re = z.im * b) ∨ 1 ≤ z.im ∧ min a b ≤ z.re ∧ z.re ≤ max a b ∧ z.im ≤ 2 + |a - b| ∧ (z.re = a ∨ z.re = b ∨ z.im = 2 + |a - b|)

Every point is either on a radial segment below the ports, or on the three-sided upper arc. The latter lies in its bounding rectangle and on its two sides or its top.

theorem Cslib.Polygonal.portLoop_contact_eq_zero {a b c d : ℝ} (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (horder : max a b < min c d ∨ max c d < min a b ∨ min a b < min c d ∧ max c d < max a b ∨ min c d < min a b ∧ max a b < max c d) (i j : Fin 5) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) (heq : (portLoop a b).eval i s = (portLoop c d).eval j t) : (portLoop a b).eval i s = 0

Disjoint or strictly nested port intervals give loops meeting only at the origin. The four port coordinates must be distinct, but neither their spacing nor the loop orientations are prescribed.

theorem Cslib.Polygonal.re_eval_portLoop_mem {a b B : ℝ} (ha : a ∈ Set.Icc 0 B) (hb : b ∈ Set.Icc 0 B) (i : Fin 5) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ((portLoop a b).eval i t).re ∈ Set.Icc 0 B

Nonnegative ports bounded by B keep every segment in the same horizontal strip.

theorem Cslib.Polygonal.atEnd_of_eval_portLoop_eq_zero {a b : ℝ} (hab : a ≠ b) (i : Fin 5) {t : ℝ} (ht : t ∈ Set.Icc 0 1) (heq : (portLoop a b).eval i t = 0) : ∃ (c : Bool), (portLoop a b).AtEnd i t c

Only the first and last global parameters of a simple port loop visit the origin.