Hyperbolic triangle orders and convex polygons

This file relates the typed elliptic-order and cusp data for a hyperbolic triangle to convex polygons in the upper half-plane. A typed triple is hyperbolic exactly when a convex triangle realises its three associated angles. The zero-angle characterization of ideal vertices then identifies the cusp entries with ideal vertices.

Main results

• TauCeti.TriangleOrder.isHyperbolic_iff_exists_interiorAngle_eq: a triple of elliptic orders and cusps is hyperbolic exactly when some convex hyperbolic triangle has the corresponding angles.
• TauCeti.UpperHalfPlane.ConvexPolygon.isRight_vertex_iff_eq_cusp: the ideal vertices of such a triangle are those at the cusp entries.

theorem TauCeti.TriangleOrder.isHyperbolic_iff_exists_interiorAngle_eq {p q r : TriangleOrder} : p.IsHyperbolic q r ↔ ∃ (P : UpperHalfPlane.ConvexPolygon 3), P.interiorAngle 0 = p.angle ∧ P.interiorAngle 1 = q.angle ∧ P.interiorAngle 2 = r.angle

Hyperbolic triangles with elliptic and cusp vertices. A triple of elliptic orders and cusps is hyperbolic exactly when some convex hyperbolic triangle has the corresponding angles: π / m at a vertex of elliptic order m, and 0 at a cusp, which is then an ideal vertex by UpperHalfPlane.ConvexPolygon.interiorAngle_eq_zero_iff.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.isRight_vertex_iff_eq_cusp {P : ConvexPolygon 3} {p q r : TriangleOrder} (hp : P.interiorAngle 0 = p.angle) (hq : P.interiorAngle 1 = q.angle) (hr : P.interiorAngle 2 = r.angle) {i : Fin 3} : (P.vertex i).isRight = true ↔ ![p, q, r] i = TriangleOrder.cusp

A vertex of a triangle with angles given by p, q, r is ideal exactly at the cusp entries.