FenchelNielsenZomorrodian/Profinite/CompactFuchsianSignature.lean
1import FenchelNielsenZomorrodian.Discrete.Core.CompactFuchsianPresentation
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Profinite/CompactFuchsianSignature.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# FenchelNielsenZomorrodian / Profinite / CompactFuchsianSignature
14Focused module in the public source tree. It contains declarations used by the library roots and by downstream proof modules.
15-/
17namespace FenchelNielsen
19universe u
21namespace ProfiniteFGroup
23/-- Promote a compact Fenchel signature with at least three periods to the compact Fuchsian
24signature used by the discrete compact three-step theorem. -/
26 (σ : FenchelSignature) (hCompact : σ.IsCompact)
27 (hPeriods : 3 ≤ σ.numPeriods) : FuchsianSignature where
28 orbitGenus := σ.orbitGenus
29 numCusps := σ.numCusps
30 numPeriods := σ.numPeriods
31 periods := σ.periods
32 period_ge_two := σ.period_ge_two
33 numCusps_eq_zero := hCompact
34 numPeriods_ge_three := hPeriods
38end FenchelNielsen