Local polygon pieces around a vertex cycle

Following the side pairings from vertex j transports it to next^[m] j by partialCycleMap j m. Pulling the polygon at that vertex back by the inverse partial product therefore gives a tile meeting the original vertex. Near a finite vertex, any finite union of these tiles agrees with the union of their pulled-back vertex sectors. In particular, the sector union contains a neighbourhood exactly when the tile union does. This reduces local vertex coverage to the angular geometry of the incident sectors, without assuming a cycle angle condition or coverage.

Consecutive sectors lie on opposite sides of their common supporting geodesic. The construction allows partial products extending beyond a full cycle, as needed when several circuits are required around an elliptic vertex.

References

Beardon, The Geometry of Discrete Groups, Chapter 9. Walkden, Hyperbolic geometry, §§17 and 19–20 (vertex cycles and the local tessellation in Poincaré's polygon theorem).

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.inv_map_smul_vertexSector_next_subset_closure_rightHalfPlane {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : (σ.map j)⁻¹ • P.vertexSector (σ.next j) ⊆ closure (rightHalfPlane (P.sideGeodesic j))

Successive pulled-back sectors are separated by the supporting geodesic of the side leaving the current vertex.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.disjoint_inv_map_smul_vertexSector_next_interior_vertexSector {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : Disjoint ((σ.map j)⁻¹ • P.vertexSector (σ.next j)) (interior (P.vertexSector j))

The interiors of consecutive vertex sectors are disjoint, including when a side is paired with itself.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.disjoint_inv_partialCycleMap_smul_vertexSector_succ_interior {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) (m : ℕ) : Disjoint ((σ.partialCycleMap j (m + 1))⁻¹ • P.vertexSector ((⇑σ.next)^[m + 1] j)) ((σ.partialCycleMap j m)⁻¹ • interior (P.vertexSector ((⇑σ.next)^[m] j)))

In the common coordinate at the initial vertex, each sector misses the interior of the preceding sector. This is adjacent-sector separation, without a claim about nonadjacent sectors.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.eventuallyEq_inv_partialCycleMap_smul_carrier_vertexSector {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) (m : ℕ) : (σ.partialCycleMap j m)⁻¹ • P.carrier =ᶠ[nhds z] (σ.partialCycleMap j m)⁻¹ • P.vertexSector ((⇑σ.next)^[m] j)

Near the initial finite vertex, every tile in a vertex cycle equals its pulled-back sector. This holds also for partial products extending beyond one circuit.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.eventuallyEq_iUnion_inv_partialCycleMap_smul_carrier_vertexSector {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) (r : ℕ) : ⋃ m ∈ Finset.range r, (σ.partialCycleMap j m)⁻¹ • P.carrier =ᶠ[nhds z] ⋃ m ∈ Finset.range r, (σ.partialCycleMap j m)⁻¹ • P.vertexSector ((⇑σ.next)^[m] j)

A finite fan of tiles along a vertex cycle locally equals its fan of sectors.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.mem_interior_iUnion_inv_partialCycleMap_smul_carrier_iff {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) (r : ℕ) : z ∈ interior (⋃ m ∈ Finset.range r, (σ.partialCycleMap j m)⁻¹ • P.carrier) ↔ z ∈ interior (⋃ m ∈ Finset.range r, (σ.partialCycleMap j m)⁻¹ • P.vertexSector ((⇑σ.next)^[m] j))

The cycle tiles cover a neighbourhood of a finite vertex if and only if their sectors cover one. No angular coverage is assumed in deriving this equivalence.