Straight fans inside a round local neighborhood

From any point strictly inside a real planar ball, the segments to distinct points on its boundary meet only at that interior point. In particular their outgoing arguments are distinct. Neither the interior point nor the circle is required to have rational coordinates.

An affine real coordinate separates two such fans and their connector when each block lies strictly beyond its own fan center. These are direct statements about all real parameters; they do not assert that a given circular block has such separating data.

theorem Cslib.Polygonal.lineMap_sphere_parameter {z a b : ℂ} {ρ t : ℝ} (ha : a ∈ Metric.ball z ρ) (hb : b ∈ Metric.sphere z ρ) (ht : t ∈ Set.Icc 0 1) (hp : (AffineMap.lineMap a b) t ∈ Metric.sphere z ρ) : t = 1

A spoke from an interior point meets the cut circle only at its boundary end. The parameter is an arbitrary real number in the full unit interval.

theorem Cslib.Polygonal.fan_contact {z a p q : ℂ} {ρ s t : ℝ} (ha : a ∈ Metric.ball z ρ) (hp : p ∈ Metric.sphere z ρ) (hq : q ∈ Metric.sphere z ρ) (hpq : p ≠ q) (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) (heq : (AffineMap.lineMap a p) s = (AffineMap.lineMap a q) t) : s = 0 ∧ t = 0

Two different boundary ports of a round ball have spokes meeting only at their common interior center. No bound on the angular span of the ports is needed.

theorem Cslib.Polygonal.arg_sub_injective_on_sphere {z a p q : ℂ} {ρ : ℝ} (ha : a ∈ Metric.ball z ρ) (hp : p ∈ Metric.sphere z ρ) (hq : q ∈ Metric.sphere z ρ) (heq : ↑(p - a).arg = ↑(q - a).arg) : p = q

Distinct round-boundary ports have distinct actual arguments when seen from any interior point. This is the geometric injectivity needed after moving a fan center.

theorem Cslib.Polygonal.fan_coordinate_le (f : ℂ →ᵃ[ℝ] ℝ) {a p : ℂ} (hp : f a < f p) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : f a ≤ f ((AffineMap.lineMap a p) t)

An affine separating coordinate keeps a spoke beyond its fan center.

theorem Cslib.Polygonal.split_spokes_ne (f : ℂ →ᵃ[ℝ] ℝ) {a b p q : ℂ} (hab : f b < f a) (hp : f a < f p) (hq : f q < f b) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) : (AffineMap.lineMap a p) s ≠ (AffineMap.lineMap b q) t

Oppositely separated spokes cannot meet, for any real segment parameters.

theorem Cslib.Polygonal.split_connector_contact (f : ℂ →ᵃ[ℝ] ℝ) {a b p : ℂ} (hab : f b < f a) (hp : f a < f p) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) (heq : (AffineMap.lineMap a p) s = (AffineMap.lineMap a b) t) : s = 0 ∧ t = 0

A spoke beyond one connector end meets the connector only at that end.