Yamaguchi Lean 4 Library
FenchelNielsenZomorrodian/Discrete/CompactFuchsian/ZeroGenus/CleanupData.lean
FenchelNielsenZomorrodian/Discrete/CompactFuchsian/ZeroGenus/CleanupData/Source

FenchelNielsenZomorrodian/Discrete/CompactFuchsian/ZeroGenus/CleanupData.lean

1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.ZeroGenus.Perfectness
2import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.ZeroGenus.SecondReductionData
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/ZeroGenus/CleanupData.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Compact zero-genus three-step proof data
15Organizes first and second reduction data, perfectness numerics, reindexing, cleanup data, and the final zero-genus three-step finite-index theorem.
16-/
18namespace FenchelNielsen
20 {tailLen p q : ℕ} (hq : 2 ≤ q) :
21 3 ≤ Fintype.card (SecondReductionTransportIndex tailLen p q) := by
22 have hcard :
23 Fintype.card (SecondReductionTransportIndex tailLen p q) =
24 2 * q + 2 + q * (p - 2) + tailLen * p * q := by
26 Fintype.card_fin, Fintype.sum_sum_type, Finset.sum_const, Finset.card_univ, smul_eq_mul, Nat.mul_comm, mul_one,
27 Fintype.card_prod, Nat.mul_left_comm, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
28 rw [hcard]
29 omega
31 {tailLen p q : ℕ} (hq : 2 ≤ q)
32 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
33 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃') (htail : ∀ j, 2 ≤ tail j)
34 (x : SecondReductionTransportIndex tailLen p q) :
35 2 ≤ secondReductionTransportPeriods (p := p) (q := q) m₁' m₂' m₃' tail x := by
36 rcases x with ⟨i, k⟩
37 cases i with
38 | inl i =>
39 fin_cases i
41 using hm₁'
43 using hm₂'
44 | inr s =>
45 cases s with
46 | inl j =>
47 fin_cases j
49 using hm₃'
51 using hm₃'
52 | inr s =>
53 cases s with
54 | inl j =>
55 exact le_trans hq
56 (Nat.le_mul_of_pos_right q (lt_of_lt_of_le (by decide : 0 < 2) hm₃'))
57 | inr jk =>
59 using htail jk.1
61 {tailLen p q : ℕ} (hq : 2 ≤ q)
62 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
63 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃') (htail : ∀ j, 2 ≤ tail j) :
66 (secondReductionTransportPeriods (p := p) (q := q) m₁' m₂' m₃' tail)
67 (secondReductionTransportPeriods_ge_two hq m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail)
70 {tailLen p q : ℕ} (hq : 2 ≤ q)
71 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
72 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃') (htail : ∀ j, 2 ≤ tail j) :
74 (secondReductionTransportSignature (p := p) hq m₁' m₂' m₃' tail
75 hm₁' hm₂' hm₃' htail).toFenchelSignature :=
76 by
79 (secondReductionTransportPeriods (p := p) (q := q) m₁' m₂' m₃' tail)
80 (secondReductionTransportPeriods_ge_two hq m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail)
86 {tailLen p q : ℕ} (hq : 2 ≤ q)
87 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
88 (hm₁' : 0 < m₁') (hm₂' : 0 < m₂') (hm₃' : 0 < m₃')
89 (htail : ∀ j, 0 < tail j) :
91 (p := p) (q := q) m₁' m₂' m₃' tail i := by
92 intro i
93 cases i with
94 | inl h =>
95 fin_cases h <;> simpa [secondReductionSourcePeriods, twoPeriods]
96 | inr rest =>
97 cases rest with
98 | inl _ =>
99 exact Nat.mul_pos (lt_of_lt_of_le (by decide : 0 < 2) hq) hm₃'
100 | inr rest =>
101 cases rest with
102 | inl _ =>
103 exact Nat.mul_pos (lt_of_lt_of_le (by decide : 0 < 2) hq) hm₃'
104 | inr jk =>
105 exact htail jk.1
108 {tailLen p q : ℕ} (hq : 2 ≤ q)
109 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
110 (hm₁' : 0 < m₁') (hm₂' : 0 < m₂') (hm₃' : 0 < m₃')
111 (htail : ∀ j, 0 < tail j) :
113 (secondReductionSourcePeriods (p := p) (q := q) m₁' m₂' m₃' tail),
115 (secondReductionSourcePeriods (p := p) (q := q) m₁' m₂' m₃' tail) i :=
117 (secondReductionSourcePeriods (p := p) (q := q) m₁' m₂' m₃' tail)
118 (secondReductionSourcePeriods_pos hq m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail)
121 {tailLen q : ℕ} (m₃' : ℕ) (tail : Fin tailLen → ℕ) :
122 Fin (tailLen + 1) → ℕ :=
123 Fin.cases (q * m₃') tail
125 {tailLen q : ℕ} (hq : 2 ≤ q) (m₃' : ℕ) (tail : Fin tailLen → ℕ)
126 (hm₃' : 0 < m₃') (htail : ∀ j, 2 ≤ tail j) :
127 ∀ j : Fin (tailLen + 1), 2 ≤ firstReductionTailIncludingThird (q := q) m₃' tail j := by
128 intro j
129 refine Fin.cases ?_ (fun k => htail k) j
130 exact le_trans hq (Nat.le_mul_of_pos_right q hm₃')
131noncomputable def finHeadInsertionEquiv {n : ℕ} (k : Fin (n + 1)) :
132 Fin (n + 1) ≃ Fin (n + 1) :=
133 Equiv.ofBijective (Fin.cases k k.succAbove) <| by
134 constructor
135 · intro a b h
136 cases a using Fin.cases with
137 | zero =>
138 cases b using Fin.cases with
139 | zero => rfl
140 | succ j =>
141 exfalso
142 exact Fin.ne_succAbove k j h
143 | succ i =>
144 cases b using Fin.cases with
145 | zero =>
146 exfalso
147 exact Fin.succAbove_ne k i h
148 | succ j =>
149 exact congrArg Fin.succ (Fin.succAbove_right_inj.mp h)
150 · intro y
151 rcases Fin.eq_self_or_eq_succAbove k y with rfl | ⟨j, rfl⟩
152 · exact ⟨0, rfl⟩
153 · exact ⟨j.succ, rfl⟩
154noncomputable def twoPointSubtypeEquiv {ι : Type*} [DecidableEq ι]
155 (i j : ι) (hij : i ≠ j) : Fin 2 ≃ {k : ι // k = i ∨ k = j} where
156 toFun k :=
157 match k with
158 | ⟨0, _⟩ => ⟨i, Or.inl rfl⟩
159 | ⟨1, _⟩ => ⟨j, Or.inr rfl⟩
160 | ⟨n + 2, h⟩ => by omega
161 invFun k := if _h : (k : ι) = i then 0 else 1
162 left_inv := by
163 intro k
164 fin_cases k
165 · simp only [↓reduceDIte, Fin.isValue, Fin.zero_eta]
166 · simp only [hij.symm, ↓reduceDIte, Fin.isValue, Fin.mk_one]
167 right_inv := by
168 intro k
169 apply Subtype.ext
170 rcases k with ⟨k, hk | hk⟩
171 · subst hk
172 simp only [↓reduceDIte, Fin.isValue]
173 · subst hk
174 simp only [hij.symm, ↓reduceDIte, Fin.isValue]
175noncomputable def notTwoSubtypeEquiv {ι : Type*}
176 (i j : ι) : {k : ι // k ≠ i ∧ k ≠ j} ≃ {k : ι // ¬ (k = i ∨ k = j)} :=
177 Equiv.subtypeEquivRight (fun _ => by simp only [ne_eq, not_or])
179 {ι : Type*} [Fintype ι] [DecidableEq ι] (i j : ι) (hij : i ≠ j) :
180 OriginalFirstReductionIndex (Fintype.card {k : ι // k ≠ i ∧ k ≠ j}) ≃ ι :=
181 (Equiv.sumCongr
183 ((Fintype.equivFin {k : ι // k ≠ i ∧ k ≠ j}).symm.trans
184 (notTwoSubtypeEquiv i j))).trans
185 (Equiv.sumCompl (fun k : ι => k = i ∨ k = j))
187 {ι : Type*} [Fintype ι] [DecidableEq ι] (i j : ι) (hij : i ≠ j) :
188 originalFirstReductionReindex i j hij (.inl 0) = i := by
189 simp only [ne_eq, originalFirstReductionReindex, twoPointSubtypeEquiv, Fin.isValue, dite_eq_ite,
190 Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_fn_mk, Equiv.coe_trans, Sum.map_inl, Equiv.sumCompl_apply_inl]
192 {ι : Type*} [Fintype ι] [DecidableEq ι] (i j : ι) (hij : i ≠ j) :
193 originalFirstReductionReindex i j hij (.inl 1) = j := by
194 simp only [ne_eq, originalFirstReductionReindex, twoPointSubtypeEquiv, Fin.isValue, dite_eq_ite,
195 Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_fn_mk, Equiv.coe_trans, Sum.map_inl, Equiv.sumCompl_apply_inl]
197 {ι : Type*} [Fintype ι] [DecidableEq ι] (i j : ι) (hij : i ≠ j)
198 (k : Fin (Fintype.card {k : ι // k ≠ i ∧ k ≠ j})) :
200 ((Fintype.equivFin {k : ι // k ≠ i ∧ k ≠ j}).symm k :
201 {k : ι // k ≠ i ∧ k ≠ j}).1 := by
202 simp only [ne_eq, originalFirstReductionReindex, notTwoSubtypeEquiv, Equiv.trans_apply, Equiv.sumCongr_apply,
203 Equiv.coe_trans, Sum.map_inr, Function.comp_apply, Equiv.sumCompl_apply_inr, Equiv.subtypeEquivRight_apply_coe]
205 p : ℕ
206 hpPrime : p.Prime
207 hp : 2 ≤ p
208 tailLen : ℕ
209 m₁' : ℕ
210 m₂' : ℕ
211 tail : Fin tailLen → ℕ
212 hm₁' : 0 < m₁'
213 hm₂' : 0 < m₂'
214 htail : ∀ j, 2 ≤ tail j
215 hTailLen : 0 < tailLen
216 reindex : OriginalFirstReductionIndex tailLen ≃ Fin σ.numPeriods
217 periods_eq :
218 ∀ x, originalFirstReductionPeriods (p := p) m₁' m₂' tail x = σ.periods (reindex x)
220 (σ : FuchsianSignature) {p : ℕ} (hpPrime : p.Prime)
221 {i j : Fin σ.numPeriods} (hij : i ≠ j)
222 (hpi : p ∣ σ.periods i) (hpj : p ∣ σ.periods j) :
224 classical
225 let tailSubtype := {k : Fin σ.numPeriods // k ≠ i ∧ k ≠ j}
226 let tailLen := Fintype.card tailSubtype
227 let tailEquiv : Fin tailLen ≃ tailSubtype := (Fintype.equivFin tailSubtype).symm
228 let tail : Fin tailLen → ℕ := fun k => σ.periods ((tailEquiv k).1)
229 have hpPos : 0 < p := hpPrime.pos
230 have hpi_period_pos : 0 < σ.periods i :=
231 lt_of_lt_of_le (by decide : 0 < 2) (σ.period_ge_two i)
232 have hpj_period_pos : 0 < σ.periods j :=
233 lt_of_lt_of_le (by decide : 0 < 2) (σ.period_ge_two j)
234 have hm₁pos : 0 < σ.periods i / p :=
235 Nat.div_pos (Nat.le_of_dvd hpi_period_pos hpi) hpPos
236 have hm₂pos : 0 < σ.periods j / p :=
237 Nat.div_pos (Nat.le_of_dvd hpj_period_pos hpj) hpPos
238 have hmul₁ : p * (σ.periods i / p) = σ.periods i := by
239 rw [Nat.mul_comm]
240 exact Nat.div_mul_cancel hpi
241 have hmul₂ : p * (σ.periods j / p) = σ.periods j := by
242 rw [Nat.mul_comm]
243 exact Nat.div_mul_cancel hpj
244 have htailLen : 0 < tailLen := by
245 have hcard0 := Fintype.card_congr (originalFirstReductionReindex i j hij)
246 have hcard : 2 + tailLen = σ.numPeriods := by
247 simpa [OriginalFirstReductionIndex, tailLen] using hcard0
248 have hsig : 3 ≤ σ.numPeriods := σ.numPeriods_ge_three
249 omega
250 exact
251 { p := p
252 hpPrime := hpPrime
253 hp := hpPrime.two_le
254 tailLen := tailLen
255 m₁' := σ.periods i / p
256 m₂' := σ.periods j / p
257 tail := tail
258 hm₁' := hm₁pos
259 hm₂' := hm₂pos
260 htail := by
261 intro k
262 exact σ.period_ge_two ((tailEquiv k).1)
263 hTailLen := htailLen
265 periods_eq := by
266 intro x
267 cases x using Sum.casesOn with
268 | inl a =>
269 fin_cases a
274 | inr k =>
275 change σ.periods ((tailEquiv k).1) =
276 σ.periods (originalFirstReductionReindex i j hij (.inr k))
278noncomputable def FirstReductionPeriodData.sourceSignature
280 originalFirstReductionSignature D.m₁' D.m₂' D.tail D.hp D.hm₁' D.hm₂' D.htail
281 D.hTailLen
283end FenchelNielsen