FenchelNielsenZomorrodian/Discrete/MainTheorem.lean
1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.SourceSubgroup
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/MainTheorem.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Discrete Fenchel-Nielsen main theorem
14This file is the public theorem entry point for the discrete compact Fuchsian part used by the
15profinite Fenchel-Nielsen bridge.
16-/
18namespace FenchelNielsen
20/-- Zero-genus compact three-step construction from explicit period data.
22This is the proof-carrying discrete main theorem used by the profinite bridge. It avoids
23re-running the perfectness-to-period-data conversion when the profinite side has already produced
24the required shared-prime pair. -/
26 (σ : FuchsianSignature)
27 (hZero : σ.orbitGenus = 0)
28 (D : FirstReductionPeriodData σ) :
29 ∃ L : Subgroup (FuchsianPresentedGroup σ),
30 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
31 SubgroupQuotientHasDerivedLengthAtMost L 3 := by
32 classical
33 let secondPrime : FirstKernelTailPrimeDivisorData D := D.tailPrimeDivisorData
34 let E : SecondStageCleanupPeriodData D secondPrime :=
35 secondStageCleanupPeriodDataOfTailPrime D secondPrime
36 let sourceEquiv₀ :
37 FuchsianPresentedGroup σ ≃* FuchsianPresentedGroup D.sourceSignature :=
38 Classical.choice (firstReductionSourceMulEquiv_exists D hZero)
39 by_cases hStrict : 2 ≤ D.m₁' ∧ 2 ≤ D.m₂' ∧ 2 ≤ E.m₃'
40 · have hStrictSubgroup :
41 ∃ L : Subgroup (FuchsianPresentedGroup E.sourceSignature),
42 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
44 E.sourceSubgroup_exists_of_canonicalReductions
45 hStrict.1 hStrict.2.1 hStrict.2.2
46 let sourceEquiv₁ :
47 FuchsianPresentedGroup D.sourceSignature ≃*
48 FuchsianPresentedGroup E.sourceSignature :=
49 Classical.choice (secondStageCleanupSourceMulEquiv_exists E)
50 let sourceEquiv :
51 FuchsianPresentedGroup σ ≃* FuchsianPresentedGroup E.sourceSignature :=
52 sourceEquiv₀.trans sourceEquiv₁
53 exact sourceSubgroup_exists_of_mulEquiv sourceEquiv hStrictSubgroup
54 · have hPeriodOne :
55 D.m₁' = 1 ∨ D.m₂' = 1 ∨ E.m₃' = 1 :=
56 E.periodOne_of_not_strict hStrict
57 have hSubgroup :
58 ∃ L : Subgroup (FuchsianPresentedGroup D.sourceSignature),
59 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
60 SubgroupQuotientHasDerivedLengthAtMost L 3 := by
61 rcases hPeriodOne with hm₁' | hm₂' | hm₃'
62 · exact
64 D hm₁'
65 · exact
67 D hm₂'
68 · have hquot : D.tail secondPrime.k / secondPrime.q = 1 := by
69 simpa [E, secondStageCleanupPeriodDataOfTailPrime] using hm₃'
70 exact
72 D (by simpa [secondPrime] using hquot)
73 exact sourceSubgroup_exists_of_mulEquiv sourceEquiv₀ hSubgroup
75end FenchelNielsen