Yamaguchi Lean 4 Library
FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/RelatorProofs.lean
FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/RelatorProofs/Source

FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/RelatorProofs.lean

1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.Relators.SourceCore
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/RelatorProofs.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Second compact zero-genus reduction
14The second explicit reduction step, with ordered target signatures, transport maps, source and target relator calculations, and quotient-basis comparison.
15-/
17namespace FenchelNielsen
20 {tailLen p q : ℕ}
21 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
22 (hp : 2 ≤ p) (hq : 2 ≤ q)
23 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
24 (htail : ∀ j, 2 ≤ tail j) : Prop :=
25 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
26 let σ :=
28 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
29 let τ :=
31 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
32 let φ :=
34 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
35 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
36 let e :=
38 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
39 let η :=
41 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
42 let x : FuchsianGenerator σ :=
44 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
45 let hZero :=
46 let i₀ :=
48 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
49 ∀ k : Fin q,
50 η
51 (e.symm
52 (⟨(FreeGroup.of x) ^ k.val * ((xWord σ i₀) ^ σ.periods i₀) *
53 ((FreeGroup.of x) ^ k.val)⁻¹, by
54 change φ
55 ((FreeGroup.of x) ^ k.val * ((xWord σ i₀) ^ σ.periods i₀) *
56 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
57 have hrφ :
58 φ ((xWord σ i₀) ^ σ.periods i₀) = 1 :=
60 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
61 ((xWord σ i₀) ^ σ.periods i₀) (Or.inl ⟨i₀, rfl⟩)
62 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
63 Subgroup.normalClosure
65 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)
66 let hOne :=
67 let i₁ :=
69 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
70 ∀ k : Fin q,
71 η
72 (e.symm
73 (⟨(FreeGroup.of x) ^ k.val * ((xWord σ i₁) ^ σ.periods i₁) *
74 ((FreeGroup.of x) ^ k.val)⁻¹, by
75 change φ
76 ((FreeGroup.of x) ^ k.val * ((xWord σ i₁) ^ σ.periods i₁) *
77 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
78 have hrφ :
79 φ ((xWord σ i₁) ^ σ.periods i₁) = 1 :=
81 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
82 ((xWord σ i₁) ^ σ.periods i₁) (Or.inl ⟨i₁, rfl⟩)
83 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
84 Subgroup.normalClosure
86 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)
87 let hMiddle :=
88 ∀ r : Fin p, ∀ k : Fin q,
89 let iMiddle :=
91 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r
92 η
93 (e.symm
94 (⟨(FreeGroup.of x) ^ k.val * ((xWord σ iMiddle) ^ σ.periods iMiddle) *
95 ((FreeGroup.of x) ^ k.val)⁻¹, by
96 change φ
97 ((FreeGroup.of x) ^ k.val * ((xWord σ iMiddle) ^ σ.periods iMiddle) *
98 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
99 have hrφ :
100 φ ((xWord σ iMiddle) ^ σ.periods iMiddle) = 1 :=
102 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
103 ((xWord σ iMiddle) ^ σ.periods iMiddle) (Or.inl ⟨iMiddle, rfl⟩)
104 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
105 Subgroup.normalClosure
107 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)
108 let hTail :=
109 ∀ b : Fin p, ∀ j : Fin tailLen, ∀ k : Fin q,
110 let iTail :=
112 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j
113 η
114 (e.symm
115 (⟨(FreeGroup.of x) ^ k.val * ((xWord σ iTail) ^ σ.periods iTail) *
116 ((FreeGroup.of x) ^ k.val)⁻¹, by
117 change φ
118 ((FreeGroup.of x) ^ k.val * ((xWord σ iTail) ^ σ.periods iTail) *
119 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
120 have hrφ :
121 φ ((xWord σ iTail) ^ σ.periods iTail) = 1 :=
123 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
124 ((xWord σ iTail) ^ σ.periods iTail) (Or.inl ⟨iTail, rfl⟩)
125 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
126 Subgroup.normalClosure
128 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)
129 let hTotal :=
130 ∀ k : Fin q,
131 η
132 (e.symm
133 (⟨(FreeGroup.of x) ^ k.val * totalRelation σ *
134 ((FreeGroup.of x) ^ k.val)⁻¹, by
135 change φ
136 ((FreeGroup.of x) ^ k.val * totalRelation σ *
137 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
138 have hrφ : φ (totalRelation σ) = 1 :=
140 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
141 (totalRelation σ) (Or.inr rfl)
142 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
143 Subgroup.normalClosure
145 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)
146 hZero ∧ hOne ∧ hMiddle ∧ hTail ∧ hTotal
148 {tailLen p q : ℕ}
149 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
150 (hp : 2 ≤ p) (hq : 2 ≤ q)
151 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
152 (htail : ∀ j, 2 ≤ tail j)
153 (hCases :
155 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) :
156 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
157 let σ :=
159 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
160 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
161 let e :=
163 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
164 let η :=
166 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
167 ∀ r ∈
171 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
172 (rels := relators σ)
174 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)),
175 η r ∈ Subgroup.normalClosure
177 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by
178 classical
180 rcases hCases with ⟨hZero, hOne, hMiddle, hTail, hTotal⟩
184 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
186 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail)
188 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
190 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)
191 hZero hOne hMiddle hTail hTotal
193end FenchelNielsen