FenchelNielsenZomorrodian.lean

1import FenchelNielsenZomorrodian.Profinite.MainTheorem

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/FenchelNielsenZomorrodian.lean

7translation_root: data/translation

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

9placement: after imports, never before imports

11/-!

12# FenchelNielsenZomorrodian

14Public root module for the stable profinite Fenchel-Nielsen formalization.

16The public API is intentionally narrowed to the profinite main theorems for torsion-free open

17subgroups. The discrete zero-genus and period-one proof stack is available through focused modules,

18while this root keeps the stable downstream import surface narrow.