Clockwise order of ports on a horizontal line

The rays from the origin to (x,1), for positive x, run clockwise as x increases. The order is proved for the actual complex arguments in the fixed plane.

theorem Cslib.Polygonal.arg_port_mem {x : ℝ} (hx : 0 < x) : { re := x, im := 1 }.arg ∈ Set.Ioo 0 (Real.pi / 2)

The argument of a positive horizontal port lies in the first quadrant.

theorem Cslib.Polygonal.arg_port_strictAnti : StrictAntiOn (fun (x : ℝ) => { re := x, im := 1 }.arg) (Set.Ioi 0)

Moving a positive port to the right strictly decreases its actual real argument.

theorem Cslib.Polygonal.sbtw_angle_of_lt {a b c : ℝ} (ha : 0 ≤ a) (hab : a < b) (hbc : b < c) (hc : c < 2 * Real.pi) : sbtw ↑a ↑b ↑c

Increasing real arguments within one turn have their literal counterclockwise order.

theorem Cslib.Polygonal.clockwise_ports {a b c : ℝ} (ha : 0 < a) (hab : a < b) (hbc : b < c) : sbtw ↑{ re := c, im := 1 }.arg ↑{ re := b, im := 1 }.arg ↑{ re := a, im := 1 }.arg

Positive ports in increasing order give the required reversed argument triple.

theorem Cslib.Polygonal.direction_port_injective {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (heq : ↑{ re := a, im := 1 }.arg = ↑{ re := b, im := 1 }.arg) : a = b

Distinct positive ports have different geometric ray directions.

theorem Cslib.Polygonal.clockwise_ports_iff {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hab : a ≠ b) (hbc : b ≠ c) (hac : a ≠ c) : sbtw ↑{ re := c, im := 1 }.arg ↑{ re := b, im := 1 }.arg ↑{ re := a, im := 1 }.arg ↔ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b

All distinct positive ports have precisely the cyclic clockwise order of their horizontal coordinates, with no reflection or choice of a new orientation.