A nonconvex separation test for Schwarz--Christoffel sides

A bounded Schwarz--Christoffel side has a known direction and positive length. For two sides, rotate the first side to the real axis. If the chord from its endpoint to the start of the second side has a strict signed height, and the second side has a weak height of the same sign, then the two sides are disjoint. The test permits changes in the sign of turning exponents and is therefore applicable to nonconvex polygonal data. It isolates the geometric separation needed to check global simplicity from finite vertex and angle information.

References

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

theorem TauCeti.disjoint_schwarzChristoffelPolygon_bounded_edgeSet_of_chord_sine {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (i j : Fin n) (hi₀ : -1 < ∑ l : Fin (n + 1) with a l = a i.castSucc, e l) (hi₁ : -1 < ∑ l : Fin (n + 1) with a l = a i.succ, e l) (hj₀ : -1 < ∑ l : Fin (n + 1) with a l = a j.castSucc, e l) (hj₁ : -1 < ∑ l : Fin (n + 1) with a l = a j.succ, e l) (hsep : 0 < (Complex.exp (-↑(schwarzChristoffelEdgeAngle a e (a i.castSucc)) * Complex.I) * (schwarzChristoffelVertex a e z₀ j.castSucc - schwarzChristoffelVertex a e z₀ i.succ)).im ∧ 0 ≤ Real.sin (schwarzChristoffelEdgeAngle a e (a j.castSucc) - schwarzChristoffelEdgeAngle a e (a i.castSucc)) ∨ (Complex.exp (-↑(schwarzChristoffelEdgeAngle a e (a i.castSucc)) * Complex.I) * (schwarzChristoffelVertex a e z₀ j.castSucc - schwarzChristoffelVertex a e z₀ i.succ)).im < 0 ∧ Real.sin (schwarzChristoffelEdgeAngle a e (a j.castSucc) - schwarzChristoffelEdgeAngle a e (a i.castSucc)) ≤ 0) : Disjoint (Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc) (Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) j.castSucc.castSucc)

Two bounded Schwarz--Christoffel sides are disjoint if the chord from the end of the first side to the beginning of the second has a strict signed height, and the second side's sine contribution has the same weak sign. The heights are measured after rotating the first side to the real axis.