FenchelNielsenZomorrodian/Discrete/FiniteIndex/SmoothQuotientData.lean

1import FenchelNielsenZomorrodian.Discrete.FiniteIndex.Smooth

2import FenchelNielsenZomorrodian.Discrete.Torsion.CompactFiniteOrder

4/-

5PUBLIC_PAGE_SNAPSHOT

6generated_at: 2026-05-27T09:47:29+09:00

7lean_source: lean4/FenchelNielsenZomorrodian/Discrete/FiniteIndex/SmoothQuotientData.lean

8translation_root: data/translation

9purpose: identifies the local data snapshot used to build pages/

10placement: after imports, never before imports

12/-!

13# Smooth quotient data for finite-index compact Fuchsian constructions

15Abbreviates the generic smooth quotient package for compact Fuchsian presentations and records the

16source-subgroup existence theorem consumed by the profinite Fenchel-Nielsen bridge.

19namespace FenchelNielsen

21/-!

22# Smooth quotient data for compact Fuchsian presentations

24The compact specialization keeps only the abbreviation and the source-subgroup existence theorem

25that is actually consumed downstream. Generic kernel, finite-index, and torsion-free wrappers are

26available from `SmoothQuotientData` and are no longer repeated here.

30 (σ : FuchsianSignature) (m : ℕ) :=

33 (Fin σ.numPeriods)

34 σ.periods

36 m

40/-- The finite smooth quotient kernel gives the finite-index torsion-free subgroup consumed by the

41compact proof route. The only nonlocal input is the approved finite-subgroup torsion frontier. -/

43 {σ : FuchsianSignature} {m : ℕ}

45 ∃ L : Subgroup (FuchsianPresentedGroup σ),

46 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧

48 SmoothQuotientData.sourceSubgroup_exists_of_finiteOrderClassification

49 D

55end FenchelNielsen