Source: FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/Relators/SourceHead.lean

1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.Relators.SourceCore

2

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/Relators/SourceHead.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

13

14The second explicit reduction step, with ordered target signatures, transport maps, source and target relator calculations, and quotient-basis comparison.

15-/

16

17namespace FenchelNielsen

18

19theorem secondReductionToTransportSecondBranch_headZero_sourceCase_mem_normalClosure

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) (k : Fin q) :

25 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩

26 let σ :=

27 secondReductionCanonicalSourceSignature

28 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

29 let φ :=

30 secondReductionCanonicalSourceFreeQuotientHom

31 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

32 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _

33 let e :=

34 secondReductionCanonicalSchreierBasisEquiv

35 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

36 let η :=

37 secondReductionCanonicalSchreierToTransportSecondBranchHom

38 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

39 let x : FuchsianGenerator σ :=

40 secondReductionCanonicalDistinguishedGenerator

41 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

42 let i₀ :=

43 secondReductionCanonicalSourceZeroIndex

44 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

45 η

46 (e.symm

47 (⟨(FreeGroup.of x) ^ k.val * ((xWord σ i₀) ^ σ.periods i₀) *

48 ((FreeGroup.of x) ^ k.val)⁻¹, by

49 change φ

50 ((FreeGroup.of x) ^ k.val * ((xWord σ i₀) ^ σ.periods i₀) *

51 ((FreeGroup.of x) ^ k.val)⁻¹) = 1

52 have hrφ :

53 φ ((xWord σ i₀) ^ σ.periods i₀) = 1 :=

54 secondReductionCanonicalSourceFreeQuotientHom_respects_relators

55 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

56 ((xWord σ i₀) ^ σ.periods i₀) (Or.inl ⟨i₀, rfl⟩)

57 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈

58 Subgroup.normalClosure

59 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

60 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

61 classical

62 dsimp

63 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩

64 let σ :=

65 secondReductionCanonicalSourceSignature

66 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

67 let τ :=

68 secondReductionTransportSignature (p := p) hq

69 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail

70 let φ :=

71 secondReductionCanonicalSourceFreeQuotientHom

72 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

73 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _

74 let e :=

75 secondReductionCanonicalSchreierBasisEquiv

76 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

77 let η :=

78 secondReductionCanonicalSchreierToTransportSecondBranchHom

79 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

80 let x : FuchsianGenerator σ :=

81 secondReductionCanonicalDistinguishedGenerator

82 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

83 let i₀ :=

84 secondReductionCanonicalSourceZeroIndex

85 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

86 let zHead :=

87 secondReductionCanonicalHeadZeroKernelElement

88 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k

89 let z : φ.ker :=

90 ⟨(FreeGroup.of x) ^ k.val * ((xWord σ i₀) ^ σ.periods i₀) *

91 ((FreeGroup.of x) ^ k.val)⁻¹, by

92 change φ

93 ((FreeGroup.of x) ^ k.val * ((xWord σ i₀) ^ σ.periods i₀) *

94 ((FreeGroup.of x) ^ k.val)⁻¹) = 1

95 have hrφ : φ ((xWord σ i₀) ^ σ.periods i₀) = 1 :=

96 secondReductionCanonicalSourceFreeQuotientHom_respects_relators

97 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

98 ((xWord σ i₀) ^ σ.periods i₀) (Or.inl ⟨i₀, rfl⟩)

99 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩

100 have hz : z = zHead ^ m₁' := by

101 apply Subtype.ext

102 change

103 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *

104 ((xWord σ i₀) ^ σ.periods i₀) *

105 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =

106 ((zHead ^ m₁' : φ.ker) : FreeGroup (FuchsianGenerator σ))

107 rw [show ((zHead ^ m₁' : φ.ker) : FreeGroup (FuchsianGenerator σ)) =

108 ((zHead : φ.ker) : FreeGroup (FuchsianGenerator σ)) ^ m₁' by

109 exact (map_pow (φ.ker.subtype) zHead m₁')]

110 simp only [secondReductionCanonicalSourceSignature, secondReductionCanonicalDistinguishedGenerator, xWord,

111 secondReductionCanonicalSourceZeroIndex, Fin.mk_zero', secondReductionCanonicalSourcePeriod, Fin.coe_ofNat_eq_mod,

112 Nat.zero_mod, ↓reduceDIte, secondReductionCanonicalHeadZeroKernelElement, Lean.Elab.WF.paramLet,

113 secondReductionCanonicalZeroImageKernelElement, id_eq, conj_pow, x, i₀, zHead, σ]

114 have hmain : (η (e.symm zHead)) ^ m₁' ∈ Subgroup.normalClosure

115 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

116 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

117 have hword :=

118 secondReductionCanonicalSchreierToTransportSecondBranchHom_headZeroWord

119 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k

120 have hrel :

121 (secondReductionCanonicalTransportTargetWord (p := p) (q := q)

122 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail

123 (secondReductionCanonicalTransportHeadIndex tailLen p q ⟨0, by decide⟩ k)) ^

124 m₁' ∈ Subgroup.normalClosure

125 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

126 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

127 have hmem :

128 (xWord τ

129 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q))

130 (secondReductionCanonicalTransportHeadIndex tailLen p q ⟨0, by decide⟩ k))) ^

131 τ.periods

132 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q))

133 (secondReductionCanonicalTransportHeadIndex tailLen p q ⟨0, by decide⟩ k)) ∈

134 secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

135 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail :=

136 secondReductionCanonicalTransport_powerRelator_mem_blockRelators

137 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail _

138 simpa [τ, secondReductionCanonicalTransportTargetWord,

139 secondReductionTransportSignature, familyFuchsianSignature_periods,

140 secondReductionTransportPeriods, singermanTransportPeriodsFamily,

141 secondReductionSourceTransportPeriods, secondReductionSourceCycleCount, twoPeriods] using

142 Subgroup.subset_normalClosure hmem

143 simpa [σ, e, η, zHead, hword] using hrel

144 change η (e.symm z) ∈ Subgroup.normalClosure

145 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

146 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)

147 rw [hz, map_pow]

148 simpa [zHead] using hmain

149theorem secondReductionToTransportSecondBranch_headOne_sourceCase_mem_normalClosure

150 {tailLen p q : ℕ}

151 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)

152 (hp : 2 ≤ p) (hq : 2 ≤ q)

153 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')

154 (htail : ∀ j, 2 ≤ tail j) (k : Fin q) :

155 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩

156 let σ :=

157 secondReductionCanonicalSourceSignature

158 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

159 let φ :=

160 secondReductionCanonicalSourceFreeQuotientHom

161 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

162 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _

163 let e :=

164 secondReductionCanonicalSchreierBasisEquiv

165 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

166 let η :=

167 secondReductionCanonicalSchreierToTransportSecondBranchHom

168 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

169 let x : FuchsianGenerator σ :=

170 secondReductionCanonicalDistinguishedGenerator

171 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

172 let i₁ :=

173 secondReductionCanonicalSourceOneIndex

174 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

175 η

176 (e.symm

177 (⟨(FreeGroup.of x) ^ k.val * ((xWord σ i₁) ^ σ.periods i₁) *

178 ((FreeGroup.of x) ^ k.val)⁻¹, by

179 change φ

180 ((FreeGroup.of x) ^ k.val * ((xWord σ i₁) ^ σ.periods i₁) *

181 ((FreeGroup.of x) ^ k.val)⁻¹) = 1

182 have hrφ :

183 φ ((xWord σ i₁) ^ σ.periods i₁) = 1 :=

184 secondReductionCanonicalSourceFreeQuotientHom_respects_relators

185 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

186 ((xWord σ i₁) ^ σ.periods i₁) (Or.inl ⟨i₁, rfl⟩)

187 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈

188 Subgroup.normalClosure

189 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

190 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

191 classical

192 dsimp

193 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩

194 let σ :=

195 secondReductionCanonicalSourceSignature

196 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

197 let τ :=

198 secondReductionTransportSignature (p := p) hq

199 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail

200 let φ :=

201 secondReductionCanonicalSourceFreeQuotientHom

202 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

203 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _

204 let e :=

205 secondReductionCanonicalSchreierBasisEquiv

206 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

207 let η :=

208 secondReductionCanonicalSchreierToTransportSecondBranchHom

209 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

210 let x : FuchsianGenerator σ :=

211 secondReductionCanonicalDistinguishedGenerator

212 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

213 let i₁ :=

214 secondReductionCanonicalSourceOneIndex

215 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

216 let zHead :=

217 secondReductionCanonicalHeadOneKernelElement

218 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k

219 let z : φ.ker :=

220 ⟨(FreeGroup.of x) ^ k.val * ((xWord σ i₁) ^ σ.periods i₁) *

221 ((FreeGroup.of x) ^ k.val)⁻¹, by

222 change φ

223 ((FreeGroup.of x) ^ k.val * ((xWord σ i₁) ^ σ.periods i₁) *

224 ((FreeGroup.of x) ^ k.val)⁻¹) = 1

225 have hrφ : φ ((xWord σ i₁) ^ σ.periods i₁) = 1 :=

226 secondReductionCanonicalSourceFreeQuotientHom_respects_relators

227 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

228 ((xWord σ i₁) ^ σ.periods i₁) (Or.inl ⟨i₁, rfl⟩)

229 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩

230 have hz : z = zHead ^ m₂' := by

231 apply Subtype.ext

232 change

233 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *

234 ((xWord σ i₁) ^ σ.periods i₁) *

235 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =

236 ((zHead ^ m₂' : φ.ker) : FreeGroup (FuchsianGenerator σ))

237 rw [show ((zHead ^ m₂' : φ.ker) : FreeGroup (FuchsianGenerator σ)) =

238 ((zHead : φ.ker) : FreeGroup (FuchsianGenerator σ)) ^ m₂' by

239 exact (map_pow (φ.ker.subtype) zHead m₂')]

240 simp only [secondReductionCanonicalSourceSignature, secondReductionCanonicalDistinguishedGenerator, xWord,

241 secondReductionCanonicalSourceOneIndex, secondReductionCanonicalSourcePeriod, one_ne_zero, ↓reduceDIte,

242 secondReductionCanonicalHeadOneKernelElement, Lean.Elab.WF.paramLet, secondReductionCanonicalZeroImageKernelElement,

243 id_eq, conj_pow, x, i₁, zHead, σ]

244 have hmain : (η (e.symm zHead)) ^ m₂' ∈ Subgroup.normalClosure

245 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

246 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

247 have hword :=

248 secondReductionCanonicalSchreierToTransportSecondBranchHom_headOneWord

249 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k

250 have hrel :

251 (secondReductionCanonicalTransportTargetWord (p := p) (q := q)

252 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail

253 (secondReductionCanonicalTransportHeadIndex tailLen p q ⟨1, by decide⟩ k)) ^

254 m₂' ∈ Subgroup.normalClosure

255 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

256 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail) := by

257 have hmem :

258 (xWord τ

259 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q))

260 (secondReductionCanonicalTransportHeadIndex tailLen p q ⟨1, by decide⟩ k))) ^

261 τ.periods

262 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q))

263 (secondReductionCanonicalTransportHeadIndex tailLen p q ⟨1, by decide⟩ k)) ∈

264 secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

265 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail :=

266 secondReductionCanonicalTransport_powerRelator_mem_blockRelators

267 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail _

268 simpa [τ, secondReductionCanonicalTransportTargetWord,

269 secondReductionTransportSignature, familyFuchsianSignature_periods,

270 secondReductionTransportPeriods, singermanTransportPeriodsFamily,

271 secondReductionSourceTransportPeriods, secondReductionSourceCycleCount, twoPeriods] using

272 Subgroup.subset_normalClosure hmem

273 simpa [σ, e, η, zHead, hword] using hrel

274 change η (e.symm z) ∈ Subgroup.normalClosure

275 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

276 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)

277 rw [hz, map_pow]

278 simpa [zHead] using hmain

279

280end FenchelNielsen