FenchelNielsenZomorrodian/Profinite.lean

1import FenchelNielsenZomorrodian.Profinite.MainTheorem

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/FenchelNielsenZomorrodian/Profinite.lean

7translation_root: data/translation

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

9placement: after imports, never before imports

11/-!

12# Profinite Fenchel groups

14Public entry point for the profinite Fenchel-Nielsen library.

16The root module intentionally exposes only the narrowed public surface:

18* profinite Fenchel group presentations and signature API;

19* existence of torsion-free open normal/characteristic subgroups;

20* the non-perfect three-step torsion-free open subgroup theorem.

22Auxiliary quotient constructions and discrete transport modules remain available through their

23specific files, but are not re-exported here.