Gaps separating two finite circular blocks

Real angle representatives in a single turn determine two actual gap points on the circle. Finite extrema choose the second gap internally. Empty blocks retain the specified cut: when one block is empty, both gaps lie in that block's empty slot.

theorem Cslib.Polygonal.sbtw_angle_cut_iff_lt {cut a b : ℝ} (ha : a ∈ Set.Ioo cut (cut + 2 * Real.pi)) (hb : b ∈ Set.Ioo cut (cut + 2 * Real.pi)) : sbtw ↑cut ↑a ↑b ↔ a < b

Cutting before two real representatives in one turn turns their circular order into their strict linear order. Equal representatives give no strict betweenness.

theorem Cslib.Polygonal.exists_gap_between_finite_blocks (A B : Finset ℂ) (θ : ℂ → ℝ) (cut : ℝ) (hA : ∀ x ∈ A, θ x ∈ Set.Ioo cut (cut + 2 * Real.pi)) (hB : ∀ x ∈ B, θ x ∈ Set.Ioo cut (cut + 2 * Real.pi)) (hAB : ∀ x ∈ A, ∀ y ∈ B, θ x < θ y) : ∃ gap ∈ Set.Ioo cut (cut + 2 * Real.pi), (∀ x ∈ A, θ x < gap) ∧ ∀ y ∈ B, gap < θ y

Two finite linearly ordered blocks in one open turn admit an intervening cut, even when either block is empty. The original cut is retained.

noncomputable def Cslib.Polygonal.circlePoint (z : ℂ) (ρ θ : ℝ) : ℂ

Boundary point with the prescribed real angle representative and radius.

theorem Cslib.Polygonal.circlePoint_mem_sphere (z : ℂ) {ρ : ℝ} (hρ : 0 ≤ ρ) (θ : ℝ) : circlePoint z ρ θ ∈ Metric.sphere z ρ

The parameterized circle point lies on its actual real metric sphere.

theorem Cslib.Polygonal.arg_circlePoint_sub (z : ℂ) {ρ : ℝ} (hρ : 0 < ρ) (θ : ℝ) : ↑(circlePoint z ρ θ - z).arg = ↑θ

The point's literal argument is the prescribed angle, without a principal-cut restriction on the real representative.

theorem Cslib.Polygonal.exists_circle_gaps_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) : ∃ gap ∈ Set.Ioo cut (cut + 2 * Real.pi), ∃ p ∈ Metric.sphere z ρ, ∃ q ∈ Metric.sphere z ρ, ↑(p - z).arg = ↑cut ∧ ↑(q - z).arg = ↑gap ∧ p ≠ q ∧ (∀ x ∈ A, θ x < gap) ∧ (∀ x ∈ B, gap < θ x) ∧ (∀ x ∈ A, sbtw ↑(p - z).arg ↑(x - z).arg ↑(q - z).arg) ∧ ∀ x ∈ B, sbtw ↑(q - z).arg ↑(x - z).arg ↑(p - z).arg

Two finite contiguous blocks on a real circle supply their own two separating gap points. The input records only their actual angle representatives and order. It supplies no geometric separator, center or connector.