Connector insertion in a prescribed circle gap

Opposite small normal offsets of a chord midpoint have a straight connector. At each offset, that connector occupies the complementary gap of its assigned circular block. The order statements compare actual complex arguments in the fixed orientation.

theorem Cslib.Polygonal.chordOffset_swap (p q : ℂ) (t : ℝ) : chordOffset q p t = chordOffset p q (-t)

Reversing the chord interchanges positive and negative normal offsets.

theorem Cslib.Polygonal.eventually_connector_order_of_circle_arc {z p q x y : ℂ} {ρ : ℝ} (hp : p ∈ Metric.sphere z ρ) (hq : q ∈ Metric.sphere z ρ) (hx : x ∈ Metric.sphere z ρ) (hy : y ∈ Metric.sphere z ρ) (hpq : p ≠ q) (hxy : x ≠ y) (hpxq : sbtw ↑(p - z).arg ↑(x - z).arg ↑(q - z).arg) (hpyq : sbtw ↑(p - z).arg ↑(y - z).arg ↑(q - z).arg) : ∀ᶠ (t : ℝ) in nhds 0, sbtw ↑(-(Complex.I * (p - midpoint ℝ p q))).arg ↑(x - chordOffset p q t).arg ↑(y - chordOffset p q t).arg ↔ sbtw ↑(p - z).arg ↑(x - z).arg ↑(y - z).arg

At all sufficiently small offsets, the connector's outgoing direction has the same position relative to two ports as the specified start of their circular block. The strict circle gaps supply this position; no connector-order premise is used.

theorem Cslib.Polygonal.exists_split_fans_of_circle_gaps {z p q : ℂ} {ρ : ℝ} (hp : p ∈ Metric.sphere z ρ) (hq : q ∈ Metric.sphere z ρ) (hpq : p ≠ q) (A B : Finset ℂ) (hA : ∀ x ∈ A, x ∈ Metric.sphere z ρ ∧ sbtw ↑(p - z).arg ↑(x - z).arg ↑(q - z).arg) (hB : ∀ x ∈ B, x ∈ Metric.sphere z ρ ∧ sbtw ↑(q - z).arg ↑(x - z).arg ↑(p - z).arg) : ∃ a ∈ Metric.ball z ρ, ∃ b ∈ Metric.ball z ρ, (chordCoordinate p q) b < (chordCoordinate p q) a ∧ (∀ x ∈ A, (chordCoordinate p q) a < (chordCoordinate p q) x) ∧ (∀ x ∈ B, (chordCoordinate p q) x < (chordCoordinate p q) b) ∧ (∀ x ∈ A, ∀ y ∈ A, x ≠ y → (sbtw ↑(b - a).arg ↑(x - a).arg ↑(y - a).arg ↔ sbtw ↑(p - z).arg ↑(x - z).arg ↑(y - z).arg)) ∧ ∀ x ∈ B, ∀ y ∈ B, x ≠ y → (sbtw ↑(a - b).arg ↑(x - b).arg ↑(y - b).arg ↔ sbtw ↑(q - z).arg ↑(x - z).arg ↑(y - z).arg)

Finite circle gaps determine two separated interior fans and a connector in the exact complementary gap at each center. Empty blocks impose no spurious order condition. All separation and connector orders are proved from the two actual circle arcs.

theorem Cslib.Polygonal.exists_split_fans_of_finite_blocks {z : ℂ} {ρ : ℝ} (hρ : 0 < ρ) (A B : Finset ℂ) (θ : ℂ → ℝ) (cut : ℝ) (hA : ∀ x ∈ A, x ∈ Metric.sphere z ρ ∧ θ x ∈ Set.Ioo cut (cut + 2 * Real.pi) ∧ ↑(x - z).arg = ↑(θ x)) (hB : ∀ x ∈ B, x ∈ Metric.sphere z ρ ∧ θ x ∈ Set.Ioo cut (cut + 2 * Real.pi) ∧ ↑(x - z).arg = ↑(θ x)) (hAB : ∀ x ∈ A, ∀ y ∈ B, θ x < θ y) : ∃ a ∈ Metric.ball z ρ, ∃ b ∈ Metric.ball z ρ, ∃ (f : ℂ →ᵃ[ℝ] ℝ), f b < f a ∧ (∀ x ∈ A, f a < f x) ∧ (∀ x ∈ B, f x < f b) ∧ (∀ x ∈ A, ∀ y ∈ A, x ≠ y → (sbtw ↑(b - a).arg ↑(x - a).arg ↑(y - a).arg ↔ θ x < θ y)) ∧ ∀ x ∈ B, ∀ y ∈ B, x ≠ y → (sbtw ↑(a - b).arg ↑(x - b).arg ↑(y - b).arg ↔ θ x < θ y)

Two finite consecutive blocks of actual circle ports determine separated interior fans and a straight connector in their prescribed insertion slots. Only the actual circle, its port order and its specified cut are inputs; all gap points, centers, the affine separator and connector order are chosen and proved internally.