Ordering nonhorizontal rays from the positive horizontal cut

Nonhorizontal vectors have real angular representatives strictly inside one turn. Within either open half-plane their order is the sign of the real planar determinant. The cut is auxiliary; the resulting circular order is the existing order on Real.Angle.

noncomputable def Cslib.Polygonal.turnArg (z : ℂ) : ℝ

Argument measured counterclockwise from the positive real ray in [0,2π). For a nonhorizontal vector it lies strictly between the endpoints.

theorem Cslib.Polygonal.arg_mem_half_turn {z : ℂ} (hz : z.im ≠ 0) : if z.im < 0 then z.arg ∈ Set.Ioo (-Real.pi) 0 else z.arg ∈ Set.Ioo 0 Real.pi

Nonhorizontal vectors avoid the argument cut and its half-turn.

theorem Cslib.Polygonal.turnArg_mem {z : ℂ} (hz : z.im ≠ 0) : turnArg z ∈ Set.Ioo 0 (2 * Real.pi)

The real representative of a nonhorizontal ray lies inside one full turn.

@[simp]

theorem Cslib.Polygonal.turnArg_coe_angle (z : ℂ) : ↑(turnArg z) = ↑z.arg

Changing the cut does not change the actual direction as a circular angle.

theorem Cslib.Polygonal.arg_lt_arg_iff_det_pos {u v : ℂ} (hu : u.im ≠ 0) (hv : v.im ≠ 0) (hsame : u.im < 0 ↔ v.im < 0) : u.arg < v.arg ↔ 0 < u.re * v.im - u.im * v.re

In either open half-plane, argument comparison is the determinant sign.

theorem Cslib.Polygonal.turnArg_lt_iff {u v : ℂ} (hu : u.im ≠ 0) (hv : v.im ≠ 0) : turnArg u < turnArg v ↔ 0 < u.im ∧ v.im < 0 ∨ (u.im < 0 ↔ v.im < 0) ∧ 0 < u.re * v.im - u.im * v.re

Comparison from the positive horizontal cut: upper rays precede lower rays, and within either half-plane the determinant gives the order.

theorem Cslib.Polygonal.sum_angularPrefix_adjacent {ι : Type u_1} [Fintype ι] (θ : ι → ℝ) (x : ι → Bool) (hθ : ∀ (i : ι), θ i ∈ Set.Ioo 0 (2 * Real.pi)) (hinj : Function.Injective θ) (heven : ∑ i : ι, x i = 0) (k l : ι) (hkl : k ≠ l) (hgap : ∀ (e : ι), e ≠ k → e ≠ l → ¬sbtw ↑(θ k) ↑(θ e) ↑(θ l)) : ∑ e : ι, x e * decide (θ e < θ k) + ∑ e : ι, x e * decide (θ e < θ l) = x k

Prefix sums of an even labeling differ by the intervening ray label across an empty counterclockwise sector. The wrap around the horizontal cut cancels by evenness.

theorem Cslib.Polygonal.sbtw_angle_add_right_iff (a b c t : Real.Angle) : sbtw (a + t) (b + t) (c + t) ↔ sbtw a b c

Circular angle order is unchanged by a common rotation.

theorem Cslib.Polygonal.sbtw_arg_mul_iff (u a b c : ℂ) (hu : u ≠ 0) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) : sbtw ↑(u * a).arg ↑(u * b).arg ↑(u * c).arg ↔ sbtw ↑a.arg ↑b.arg ↑c.arg

Multiplication by a nonzero complex number preserves literal circular ray order.