Circular order for moving local fan centers

Moving the center anywhere inside a circle preserves the literal circular order of its distinct boundary ports. The proof uses local real representatives and convex connectedness of the ball. The cut of the turn can be anywhere; no principal-argument branch or rational-coordinate hypothesis is imposed. No ambient map or PL transport is assumed.

theorem Cslib.Polygonal.sbtw_angle_iff_cyclic_lt {cut a b c : ℝ} (ha : a ∈ Set.Ioo cut (cut + 2 * Real.pi)) (hb : b ∈ Set.Ioo cut (cut + 2 * Real.pi)) (hc : c ∈ Set.Ioo cut (cut + 2 * Real.pi)) (hab : a ≠ b) (hbc : b ≠ c) (hac : a ≠ c) : sbtw ↑a ↑b ↑c ↔ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b

Three distinct real representatives in any one turn have exactly their cyclic linear order as angles. In particular the cut may cross the principal argument branch.

theorem Cslib.Polygonal.eventually_sbtw_angle_iff {X : Type u_1} [TopologicalSpace X] {x : X} {f g h : X → Real.Angle} (hf : ContinuousAt f x) (hg : ContinuousAt g x) (hh : ContinuousAt h x) (hfg : f x ≠ g x) (hgh : g x ≠ h x) (hfh : f x ≠ h x) : ∀ᶠ (y : X) in nhds x, sbtw (f y) (g y) (h y) ↔ sbtw (f x) (g x) (h x)

Strict order of three distinct continuously varying angles is stable in a neighborhood. The proof chooses its own common argument cut and includes principal-branch crossings; pairwise distinctness is required only at the point under consideration.

theorem Cslib.Polygonal.sbtw_arg_sub_iff_of_mem_ball {z a b p q r : ℂ} {ρ : ℝ} (ha : a ∈ Metric.ball z ρ) (hb : b ∈ Metric.ball z ρ) (hp : p ∈ Metric.sphere z ρ) (hq : q ∈ Metric.sphere z ρ) (hr : r ∈ Metric.sphere z ρ) (hpq : p ≠ q) (hqr : q ≠ r) (hpr : p ≠ r) : sbtw ↑(p - a).arg ↑(q - a).arg ↑(r - a).arg ↔ sbtw ↑(p - b).arg ↑(q - b).arg ↑(r - b).arg

Moving a fan center anywhere inside its cut circle preserves the literal circular order of three distinct boundary ports. This includes all argument branches and makes no semicircle assumption about the ports. It concerns finite straight spokes, not an ambient homeomorphism or a topological drawing theorem.