Cusp data at ideal vertices of a convex polygon

For a polygon whose ideal vertices are cusp points of a discrete subgroup, choose normalized cusp data at each ideal vertex. Their scalings extend to a family indexed by all vertices and carry each ideal vertex to infinity.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.exists_cuspDatum_scaling {n : ℕ} [NeZero n] (P : ConvexPolygon n) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (hcusp : ∀ (i : Fin n) (c : OnePoint ℝ), P.vertex i = Sum.inr c → Γ.IsCuspPoint c) : ∃ (D : { i : Fin n // (P.vertex i).isRight = true } → Γ.CuspDatum), (∀ (i : { i : Fin n // (P.vertex i).isRight = true }), P.vertex ↑i = Sum.inr (D i).cusp) ∧ ∃ (g : Fin n → Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ), (∀ (i : Fin n) (hi : (P.vertex i).isRight = true), g i = (D ⟨i, hi⟩).scaling) ∧ ∀ (i : Fin n) (c : OnePoint ℝ), P.vertex i = Sum.inr c → g i • c = OnePoint.infty

Cusp data at the ideal vertices, together with scalings sending those vertices to infinity. The scalings agree with the chosen cusp data at ideal vertices; finite vertices require no data.