Separating nonconvex Schwarz--Christoffel sides from the closing sides

The total turning exponent -2 puts the first finite vertex, the last finite vertex, and the vertex at infinity on one horizontal line. If every intermediate vertex lies strictly above this line, a bounded polygon side can meet either closing side only at their common finite endpoint. This condition allows reentrant corners: the bounded sides need not have monotone directions.

Together with a check that nonadjacent bounded sides do not meet, this gives a finite geometric criterion for simplicity of the compactified boundary and hence for the primitive to map the upper half-plane bijectively onto the complementary component containing its base-point image.

References

• L. Ahlfors, Complex Analysis, Ch. 6, Section 2.
• T. Driscoll and L. Trefethen, Schwarz--Christoffel Mapping, Ch. 2.

theorem TauCeti.schwarzChristoffelPolygon_bounded_edgeSet_last_eq_first_vertex_of_heights {n : ℕ} (a e : Fin (n + 2) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (he : ∀ (k : Fin (n + 2)), -1 < e k) (hsum : ∑ k : Fin (n + 2), e k = -2) (hheight : ∀ (k : Fin (n + 2)), k ≠ 0 → k ≠ Fin.last (n + 1) → (schwarzChristoffelVertex a e z₀ 0).im < (schwarzChristoffelVertex a e z₀ k).im) (i : Fin (n + 1)) (z : ℂ) (hzi : z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc) (hzleft : z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) (Fin.last (n + 2))) : z = schwarzChristoffelVertex a e z₀ 0

If all intermediate vertices are strictly above the horizontal closing line, a bounded side meets the left closing side only at the first finite vertex.

theorem TauCeti.schwarzChristoffelPolygon_bounded_edgeSet_last_prevertex_eq_last_vertex_of_heights {n : ℕ} (a e : Fin (n + 2) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (he : ∀ (k : Fin (n + 2)), -1 < e k) (hsum : ∑ k : Fin (n + 2), e k = -2) (hheight : ∀ (k : Fin (n + 2)), k ≠ 0 → k ≠ Fin.last (n + 1) → (schwarzChristoffelVertex a e z₀ 0).im < (schwarzChristoffelVertex a e z₀ k).im) (i : Fin (n + 1)) (z : ℂ) (hzi : z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc) (hzright : z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) (Fin.last (n + 1)).castSucc) : z = schwarzChristoffelVertex a e z₀ (Fin.last (n + 1))

If all intermediate vertices are strictly above the horizontal closing line, a bounded side meets the right closing side only at the last finite vertex.