A simple Schwarz--Christoffel boundary is locally straight at regular edges

On an interval free of turning prevertices, the Schwarz--Christoffel boundary traces an open line segment. If the compactified boundary is simple, compactness prevents any other part of the curve from accumulating at an interior point of that segment. Thus, in a small ball, the entire curve agrees with the open segment. This identifies the local geometry needed to select the bounded component of the polygonal complement.

The argument follows the polygonal-boundary viewpoint of Driscoll and Trefethen, Schwarz--Christoffel Mapping, Chapter 2.

theorem TauCeti.schwarzChristoffelCompactifiedBoundary_locally_openSegment {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q x : ℝ} (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hinfty : ∑ i : ι, e i < -1) (hinj : Function.Injective (schwarzChristoffelCompactifiedBoundary a e z₀)) (hx : x ∈ Set.Ioo p q) : ∃ (ε : ℝ), 0 < ε ∧ Set.range (schwarzChristoffelCompactifiedBoundary a e z₀) ∩ Metric.ball (schwarzChristoffelBoundary a e z₀ x) ε = openSegment ℝ (schwarzChristoffelBoundary a e z₀ p) (schwarzChristoffelBoundary a e z₀ q) ∩ Metric.ball (schwarzChristoffelBoundary a e z₀ x) ε

Near the image of a point strictly inside a regular edge, a simple compactified Schwarz--Christoffel boundary consists precisely of that open straight edge.