Closing-side separation from vertex heights

For a Schwarz--Christoffel polygon with possibly reentrant corners, strict height of every intermediate vertex above the horizontal closing line keeps the bounded sides away from both closing sides except at their prescribed endpoints. Together with a bounded-side intersection check, this proves simplicity of the compactified boundary. The height condition is finite and geometric, so it can be checked independently of the analytic construction of the vertices.

References

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

theorem TauCeti.schwarzChristoffelPolygon_bounded_edgeSet_eq_endpoint_of_im_le {n : ℕ} (a e : Fin (n + 3) → ℝ) (z₀ : UpperHalfPlane) (hends : (schwarzChristoffelVertex a e z₀ (Fin.last (n + 2))).im = (schwarzChristoffelVertex a e z₀ 0).im) (hheight : ∀ (k : Fin (n + 3)), k ≠ 0 → k ≠ Fin.last (n + 2) → (schwarzChristoffelVertex a e z₀ 0).im < (schwarzChristoffelVertex a e z₀ k).im) (i : Fin (n + 2)) {z : ℂ} (hz : z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc) (hzim : z.im ≤ (schwarzChristoffelVertex a e z₀ 0).im) : z = schwarzChristoffelVertex a e z₀ 0 ∨ z = schwarzChristoffelVertex a e z₀ (Fin.last (n + 2))

If every intermediate vertex is strictly above the line through the first and last vertices, a bounded side can meet that line only at one of those two endpoints.

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

Strict intermediate vertex heights discharge both closing-side intersection hypotheses of the polygonal simplicity criterion. The exponents may be positive.

theorem TauCeti.schwarzChristoffelCompactifiedBoundary_injective_of_bounded_intersections_of_vertex_heights {n : ℕ} (a e : Fin (n + 3) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (he : ∀ (k : Fin (n + 3)), -1 < e k) (hsum : ∑ k : Fin (n + 3), e k = -2) (hheight : ∀ (k : Fin (n + 3)), k ≠ 0 → k ≠ Fin.last (n + 2) → (schwarzChristoffelVertex a e z₀ 0).im < (schwarzChristoffelVertex a e z₀ k).im) (hbounded : ∀ (i j : Fin (n + 2)), i < j → ∀ z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc, z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) j.castSucc.castSucc → ↑j = ↑i + 1 ∧ z = schwarzChristoffelVertex a e z₀ i.succ) : Function.Injective (schwarzChristoffelCompactifiedBoundary a e z₀)

A bounded-side intersection check and strict interior vertex heights make the compactified Schwarz--Christoffel boundary simple, including for reentrant corners.