Circle chords and affine separation

The midpoint of a chord is an interior point of the circle. The two open circular arcs cut out by its endpoints are exactly the two strict affine half-planes of the chord. This works for both major and minor arcs, including a diameter.

theorem Cslib.Polygonal.sbtw_zero_arg_pi_iff (w : ℂ) : sbtw 0 ↑w.arg ↑Real.pi ↔ 0 < w.im

The open upper half-plane is the strict angle interval from zero to pi.

theorem Cslib.Polygonal.midpoint_mem_ball_of_mem_sphere {z p q : ℂ} {ρ : ℝ} (hp : p ∈ Metric.sphere z ρ) (hq : q ∈ Metric.sphere z ρ) (hpq : p ≠ q) : midpoint ℝ p q ∈ Metric.ball z ρ

Two distinct points on a circle have a chord midpoint strictly inside it.

noncomputable def Cslib.Polygonal.chordCoordinate (p q : ℂ) : ℂ →ᵃ[ℝ] ℝ

The signed coordinate perpendicular to a chord, scaled so its normal has unit coordinate. The first endpoint fixes the sign; its counterclockwise arc is positive.

theorem Cslib.Polygonal.sbtw_arg_iff_chordCoordinate_pos {z p q x : ℂ} {ρ : ℝ} (hp : p ∈ Metric.sphere z ρ) (hq : q ∈ Metric.sphere z ρ) (hx : x ∈ Metric.sphere z ρ) (hpq : p ≠ q) (hpx : p ≠ x) (hxq : x ≠ q) : sbtw ↑(p - z).arg ↑(x - z).arg ↑(q - z).arg ↔ 0 < (chordCoordinate p q) x

A circle arc has exactly the sign of its chord's affine coordinate. All real coordinates are retained, with no angular-span restriction.

theorem Cslib.Polygonal.chordCoordinate_swap (p q : ℂ) : chordCoordinate q p = -chordCoordinate p q

Reversing the oriented chord reverses its affine coordinate.

noncomputable def Cslib.Polygonal.chordOffset (p q : ℂ) (t : ℝ) : ℂ

Offset the chord midpoint in its oriented normal direction.

theorem Cslib.Polygonal.exists_split_offsets_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) {bound : ℝ} (hbound : 0 < bound) : ∃ ε ∈ Set.Ioo 0 bound, chordOffset p q ε ∈ Metric.ball z ρ ∧ chordOffset p q (-ε) ∈ Metric.ball z ρ ∧ (chordCoordinate p q) (chordOffset p q (-ε)) < (chordCoordinate p q) (chordOffset p q ε) ∧ (∀ x ∈ A, (chordCoordinate p q) (chordOffset p q ε) < (chordCoordinate p q) x) ∧ ∀ x ∈ B, (chordCoordinate p q) x < (chordCoordinate p q) (chordOffset p q (-ε))

A finite collection on the two open arcs of a circle admits arbitrarily small opposite interior offsets strictly separated from their assigned ports. Either port set may be empty. The offsets and affine separator are constructed from the circle and gaps.