FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/OrderedTargetSignature.lean
1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.Signatures
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/OrderedTargetSignature.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
14The second explicit reduction step, with ordered target signatures, transport maps, source and target relator calculations, and quotient-basis comparison.
15-/
17namespace FenchelNielsen
18def secondReductionCanonicalOrderedTargetBlockLen (tailLen p : ℕ) : ℕ :=
19 2 + ((p - 2) + p * tailLen)
20def secondReductionCanonicalOrderedTargetNumPeriods (tailLen p q : ℕ) : ℕ :=
21 2 + q * secondReductionCanonicalOrderedTargetBlockLen tailLen p
23 (tailLen p q : ℕ) (d : Fin 2) :
24 Fin (secondReductionCanonicalOrderedTargetNumPeriods tailLen p q) :=
25 ⟨d.val, by
26 have hd := d.isLt
27 simp only [secondReductionCanonicalOrderedTargetNumPeriods, secondReductionCanonicalOrderedTargetBlockLen,
28 gt_iff_lt]
29 omega⟩
31 (tailLen p q : ℕ) (h : Fin 2) (k : Fin q) :
32 Fin (secondReductionCanonicalOrderedTargetNumPeriods tailLen p q) :=
33 ⟨2 + k.val * secondReductionCanonicalOrderedTargetBlockLen tailLen p +
34 (p - 2) + p * tailLen + h.val, by
35 let L := secondReductionCanonicalOrderedTargetBlockLen tailLen p
36 have hpos : (p - 2) + p * tailLen + h.val < L := by
37 have hh := h.isLt
38 dsimp [L, secondReductionCanonicalOrderedTargetBlockLen]
39 omega
40 have hblock :
41 k.val * L + ((p - 2) + p * tailLen + h.val) < (k.val + 1) * L := by
42 calc
43 k.val * L + ((p - 2) + p * tailLen + h.val) < k.val * L + L :=
44 Nat.add_lt_add_left hpos _
45 _ = (k.val + 1) * L := by rw [Nat.add_mul, one_mul]
46 have hle : (k.val + 1) * L ≤ q * L :=
47 Nat.mul_le_mul_right L (Nat.succ_le_of_lt k.isLt)
48 have hlt' : 2 + (k.val * L + ((p - 2) + p * tailLen + h.val)) < 2 + q * L :=
49 Nat.add_lt_add_left (lt_of_lt_of_le hblock hle) 2
50 have hlt : 2 + k.val * L + ((p - 2) + p * tailLen + h.val) < 2 + q * L := by
51 simpa [Nat.add_assoc] using hlt'
52 simpa [secondReductionCanonicalOrderedTargetNumPeriods, L, Nat.add_assoc] using hlt⟩
54 (tailLen p q : ℕ) (r : Fin (p - 2)) (k : Fin q) :
55 Fin (secondReductionCanonicalOrderedTargetNumPeriods tailLen p q) :=
56 ⟨2 + k.val * secondReductionCanonicalOrderedTargetBlockLen tailLen p + r.val, by
57 let L := secondReductionCanonicalOrderedTargetBlockLen tailLen p
58 have hrL : r.val < L := by
59 have hr := r.isLt
60 dsimp [L, secondReductionCanonicalOrderedTargetBlockLen]
61 omega
62 have hblock :
63 k.val * L + r.val < (k.val + 1) * L := by
64 calc
65 k.val * L + r.val < k.val * L + L :=
66 Nat.add_lt_add_left hrL _
67 _ = (k.val + 1) * L := by rw [Nat.add_mul, one_mul]
68 have hle : (k.val + 1) * L ≤ q * L :=
69 Nat.mul_le_mul_right L (Nat.succ_le_of_lt k.isLt)
70 have hlt' : 2 + (k.val * L + r.val) < 2 + q * L :=
71 Nat.add_lt_add_left (lt_of_lt_of_le hblock hle) 2
72 have hlt : 2 + k.val * L + r.val < 2 + q * L := by
73 simpa [Nat.add_assoc] using hlt'
74 simpa [secondReductionCanonicalOrderedTargetNumPeriods, L, Nat.add_assoc] using hlt⟩
76 (tailLen p q : ℕ) (b : Fin p) (j : Fin tailLen) (k : Fin q) :
77 Fin (secondReductionCanonicalOrderedTargetNumPeriods tailLen p q) :=
78 ⟨2 + k.val * secondReductionCanonicalOrderedTargetBlockLen tailLen p +
79 (p - 2) + b.val * tailLen + j.val, by
80 let L := secondReductionCanonicalOrderedTargetBlockLen tailLen p
81 have htailLen : 0 < tailLen := lt_of_le_of_lt (Nat.zero_le _) j.isLt
82 have hbj :
83 b.val * tailLen + j.val < p * tailLen := by
84 have hblock : b.val * tailLen + j.val < (b.val + 1) * tailLen := by
85 calc
86 b.val * tailLen + j.val < b.val * tailLen + tailLen :=
87 Nat.add_lt_add_left j.isLt _
88 _ = (b.val + 1) * tailLen := by rw [Nat.add_mul, one_mul]
89 have hle : (b.val + 1) * tailLen ≤ p * tailLen :=
90 Nat.mul_le_mul_right tailLen (Nat.succ_le_of_lt b.isLt)
91 exact lt_of_lt_of_le hblock hle
92 have hpos :
93 (p - 2) + (b.val * tailLen + j.val) < L := by
94 dsimp [L, secondReductionCanonicalOrderedTargetBlockLen]
95 omega
96 have hblock :
97 k.val * L + ((p - 2) + b.val * tailLen + j.val) <
98 (k.val + 1) * L := by
99 calc
100 k.val * L + ((p - 2) + b.val * tailLen + j.val) =
101 k.val * L + ((p - 2) + (b.val * tailLen + j.val)) := by omega
102 _ < k.val * L + L := Nat.add_lt_add_left hpos _
103 _ = (k.val + 1) * L := by rw [Nat.add_mul, one_mul]
104 have hle : (k.val + 1) * L ≤ q * L :=
105 Nat.mul_le_mul_right L (Nat.succ_le_of_lt k.isLt)
106 have hlt' :
107 2 + (k.val * L + ((p - 2) + b.val * tailLen + j.val)) <
108 2 + q * L :=
109 Nat.add_lt_add_left (lt_of_lt_of_le hblock hle) 2
110 have hlt :
111 2 + k.val * L + ((p - 2) + b.val * tailLen + j.val) <
112 2 + q * L := by
113 simpa [Nat.add_assoc] using hlt'
114 simpa [secondReductionCanonicalOrderedTargetNumPeriods, L, Nat.add_assoc] using hlt⟩
116 {tailLen p q : ℕ}
117 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
118 (i : Fin (secondReductionCanonicalOrderedTargetNumPeriods tailLen p q)) : ℕ :=
119 if _h0 : i.val = 0 then
120 m₃'
121 else if _h1 : i.val = 1 then
122 m₃'
123 else
124 let L := secondReductionCanonicalOrderedTargetBlockLen tailLen p
125 let r := (i.val - 2) % L
126 if _hrMid : r < p - 2 then
127 q * m₃'
128 else if _hrTail : r < (p - 2) + p * tailLen then
129 if hTailLen : 0 < tailLen then
130 tail ⟨(r - (p - 2)) % tailLen, Nat.mod_lt _ hTailLen⟩
131 else
132 m₁'
133 else if _hrHead0 : r = (p - 2) + p * tailLen then
134 m₁'
135 else
136 m₂'
138 {tailLen p q : ℕ}
139 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
140 (hp : 2 ≤ p) (hq : 2 ≤ q)
141 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
142 (htail : ∀ j, 2 ≤ tail j) :
143 FuchsianSignature where
144 orbitGenus := 0
145 numCusps := 0
146 numPeriods := secondReductionCanonicalOrderedTargetNumPeriods tailLen p q
147 periods :=
148 secondReductionCanonicalOrderedTargetPeriod (tailLen := tailLen) (p := p) (q := q)
149 m₁' m₂' m₃' tail
150 period_ge_two := by
151 intro i
152 by_cases h0 : i.val = 0
153 · simpa [secondReductionCanonicalOrderedTargetPeriod, h0] using hm₃'
154 by_cases h1 : i.val = 1
155 · simpa [secondReductionCanonicalOrderedTargetPeriod, h0, h1] using hm₃'
156 let L := secondReductionCanonicalOrderedTargetBlockLen tailLen p
157 let r := (i.val - 2) % L
158 by_cases hrMid : r < p - 2
159 · have hm₃mul : 2 ≤ q * m₃' :=
160 le_trans hq
161 (Nat.le_mul_of_pos_right q (lt_of_lt_of_le (by decide : 0 < 2) hm₃'))
162 simpa [secondReductionCanonicalOrderedTargetPeriod, h0, h1, L, r, hrMid] using hm₃mul
163 by_cases hrTail : r < (p - 2) + p * tailLen
164 · by_cases hTailLen : 0 < tailLen
165 · have htail' :
166 2 ≤ tail ⟨(r - (p - 2)) % tailLen, Nat.mod_lt _ hTailLen⟩ :=
167 htail _
168 simpa [secondReductionCanonicalOrderedTargetPeriod, h0, h1, L, r, hrMid,
169 hrTail, hTailLen] using htail'
170 · simpa [secondReductionCanonicalOrderedTargetPeriod, h0, h1, L, r, hrMid,
171 hrTail, hTailLen] using hm₁'
172 · by_cases hrHead0 : r = (p - 2) + p * tailLen
173 · simpa [secondReductionCanonicalOrderedTargetPeriod, h0, h1, L, r, hrMid,
174 hrTail, hrHead0] using hm₁'
175 · simpa [secondReductionCanonicalOrderedTargetPeriod, h0, h1, L, r, hrMid,
176 hrTail, hrHead0] using hm₂'
177 numCusps_eq_zero := rfl
178 numPeriods_ge_three := by
179 have _hp0 : 0 < p := lt_of_lt_of_le (by decide : 0 < 2) hp
180 have hq0 : 0 < q := lt_of_lt_of_le (by decide : 0 < 2) hq
181 have hL0 : 0 < secondReductionCanonicalOrderedTargetBlockLen tailLen p := by
182 simp only [secondReductionCanonicalOrderedTargetBlockLen, add_pos_iff, Nat.ofNat_pos, tsub_pos_iff_lt,
183 CanonicallyOrderedAdd.mul_pos, true_or]
184 have hprod : 0 < q * secondReductionCanonicalOrderedTargetBlockLen tailLen p :=
185 Nat.mul_pos hq0 hL0
187 omega
188@[simp 900] theorem secondReductionCanonicalOrderedTargetSignature_period_distinguished
189 {tailLen p q : ℕ}
190 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
191 (hp : 2 ≤ p) (hq : 2 ≤ q)
192 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
193 (htail : ∀ j, 2 ≤ tail j) (d : Fin 2) :
195 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).periods
196 (secondReductionCanonicalOrderedTargetDistinguishedIndex tailLen p q d) =
197 m₃' := by
198 fin_cases d <;>
199 simp only [secondReductionCanonicalOrderedTargetSignature,
200 secondReductionCanonicalOrderedTargetDistinguishedIndex, secondReductionCanonicalOrderedTargetPeriod, one_ne_zero,
201 ↓reduceDIte]
202@[simp 900] theorem secondReductionCanonicalOrderedTargetSignature_period_middleRest
203 {tailLen p q : ℕ}
204 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
205 (hp : 2 ≤ p) (hq : 2 ≤ q)
206 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
207 (htail : ∀ j, 2 ≤ tail j) (r : Fin (p - 2)) (k : Fin q) :
209 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).periods
210 (secondReductionCanonicalOrderedTargetMiddleRestIndex tailLen p q r k) =
211 q * m₃' := by
212 let L := secondReductionCanonicalOrderedTargetBlockLen tailLen p
213 have hrL : r.val < L := by
214 have hr := r.isLt
215 dsimp [L, secondReductionCanonicalOrderedTargetBlockLen]
216 omega
217 have hmod : (2 + k.val * L + r.val - 2) % L = r.val := by
218 have hsub : 2 + k.val * L + r.val - 2 = k.val * L + r.val := by omega
219 rw [hsub, Nat.mul_comm k.val L, Nat.mul_add_mod_self_left, Nat.mod_eq_of_lt hrL]
220 have hnot0 : ¬ 2 + k.val * L + r.val = 0 := by omega
221 have hnot1 : ¬ 2 + k.val * L + r.val = 1 := by omega
222 have hrMid : r.val < p - 2 := r.isLt
223 simp only [secondReductionCanonicalOrderedTargetSignature,
224 secondReductionCanonicalOrderedTargetMiddleRestIndex, secondReductionCanonicalOrderedTargetPeriod,
225 Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, mul_eq_zero, false_and, ↓reduceDIte, hnot1, hmod, hrMid, L]
226@[simp 900] theorem secondReductionCanonicalOrderedTargetSignature_period_tail
227 {tailLen p q : ℕ}
228 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
229 (hp : 2 ≤ p) (hq : 2 ≤ q)
230 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
231 (htail : ∀ j, 2 ≤ tail j) (b : Fin p) (j : Fin tailLen) (k : Fin q) :
233 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).periods
234 (secondReductionCanonicalOrderedTargetTailIndex tailLen p q b j k) =
235 tail j := by
236 let L := secondReductionCanonicalOrderedTargetBlockLen tailLen p
237 have htailLen : 0 < tailLen := lt_of_le_of_lt (Nat.zero_le _) j.isLt
238 have hbj : b.val * tailLen + j.val < p * tailLen := by
239 have hblock : b.val * tailLen + j.val < (b.val + 1) * tailLen := by
240 calc
241 b.val * tailLen + j.val < b.val * tailLen + tailLen :=
242 Nat.add_lt_add_left j.isLt _
243 _ = (b.val + 1) * tailLen := by rw [Nat.add_mul, one_mul]
244 have hle : (b.val + 1) * tailLen ≤ p * tailLen :=
245 Nat.mul_le_mul_right tailLen (Nat.succ_le_of_lt b.isLt)
246 exact lt_of_lt_of_le hblock hle
247 have hpos : (p - 2) + b.val * tailLen + j.val < L := by
248 dsimp [L, secondReductionCanonicalOrderedTargetBlockLen]
249 omega
250 have hmod :
251 (2 + k.val * L + ((p - 2) + b.val * tailLen + j.val) - 2) % L =
252 (p - 2) + b.val * tailLen + j.val := by
253 have hsub :
254 2 + k.val * L + ((p - 2) + b.val * tailLen + j.val) - 2 =
255 k.val * L + ((p - 2) + b.val * tailLen + j.val) := by omega
256 rw [hsub, Nat.mul_comm k.val L, Nat.mul_add_mod_self_left, Nat.mod_eq_of_lt hpos]
257 have hnot0 : ¬ 2 + k.val * L + ((p - 2) + b.val * tailLen + j.val) = 0 := by omega
258 have hnot1 : ¬ 2 + k.val * L + ((p - 2) + b.val * tailLen + j.val) = 1 := by omega
259 have hnotMid : ¬ (p - 2) + b.val * tailLen + j.val < p - 2 := by omega
260 have hTail : (p - 2) + b.val * tailLen + j.val < (p - 2) + p * tailLen := by
261 omega
262 have htailIndex :
263 ((p - 2) + b.val * tailLen + j.val - (p - 2)) % tailLen = j.val := by
264 have hsub : (p - 2) + b.val * tailLen + j.val - (p - 2) =
265 b.val * tailLen + j.val := by omega
266 rw [hsub, Nat.mul_comm b.val tailLen, Nat.mul_add_mod_self_left,
267 Nat.mod_eq_of_lt j.isLt]
268 have hnot1Actual :
269 ¬ 2 + k.val * L + (p - 2) + b.val * tailLen + j.val = 1 := by omega
270 have hmodActual :
271 (2 + k.val * L + (p - 2) + b.val * tailLen + j.val - 2) % L =
272 (p - 2) + b.val * tailLen + j.val := by
273 rw [show 2 + k.val * L + (p - 2) + b.val * tailLen + j.val - 2 =
274 2 + k.val * L + ((p - 2) + b.val * tailLen + j.val) - 2 by omega]
275 exact hmod
276 have htailIndexActual :
277 ((2 + k.val * L + (p - 2) + b.val * tailLen + j.val - 2) % L -
278 (p - 2)) % tailLen = j.val := by
279 rw [hmodActual]
280 exact htailIndex
283 secondReductionCanonicalOrderedTargetPeriod, L, hnot1Actual, hmodActual, hnotMid,
284 hTail, htailLen, htailIndexActual] using congrArg tail (Fin.ext htailIndex)
285@[simp 900] theorem secondReductionCanonicalOrderedTargetSignature_period_head_zero
286 {tailLen p q : ℕ}
287 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
288 (hp : 2 ≤ p) (hq : 2 ≤ q)
289 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
290 (htail : ∀ j, 2 ≤ tail j) (k : Fin q) :
292 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).periods
293 (secondReductionCanonicalOrderedTargetHeadIndex tailLen p q ⟨0, by decide⟩ k) =
294 m₁' := by
295 let L := secondReductionCanonicalOrderedTargetBlockLen tailLen p
296 have hpos : (p - 2) + p * tailLen < L := by
297 dsimp [L, secondReductionCanonicalOrderedTargetBlockLen]
298 omega
299 have hmod :
300 (2 + k.val * L + ((p - 2) + p * tailLen) - 2) % L =
301 (p - 2) + p * tailLen := by
302 have hsub :
303 2 + k.val * L + ((p - 2) + p * tailLen) - 2 =
304 k.val * L + ((p - 2) + p * tailLen) := by omega
305 rw [hsub, Nat.mul_comm k.val L, Nat.mul_add_mod_self_left, Nat.mod_eq_of_lt hpos]
306 have hnot1Actual : ¬ 2 + k.val * L + (p - 2) + p * tailLen = 1 := by omega
307 have hmodActual :
308 (2 + k.val * L + (p - 2) + p * tailLen - 2) % L =
309 (p - 2) + p * tailLen := by
310 rw [show 2 + k.val * L + (p - 2) + p * tailLen - 2 =
311 2 + k.val * L + ((p - 2) + p * tailLen) - 2 by omega]
312 exact hmod
313 have hnotMid : ¬ (p - 2) + p * tailLen < p - 2 := by omega
314 have hnotTail : ¬ (p - 2) + p * tailLen < (p - 2) + p * tailLen := by omega
315 simp only [secondReductionCanonicalOrderedTargetSignature, secondReductionCanonicalOrderedTargetHeadIndex,
316 add_zero, secondReductionCanonicalOrderedTargetPeriod, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, mul_eq_zero,
317 false_and, ↓reduceDIte, hnot1Actual, hmodActual, hnotMid, lt_self_iff_false, L]
318@[simp 900] theorem secondReductionCanonicalOrderedTargetSignature_period_head_one
319 {tailLen p q : ℕ}
320 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
321 (hp : 2 ≤ p) (hq : 2 ≤ q)
322 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
323 (htail : ∀ j, 2 ≤ tail j) (k : Fin q) :
325 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).periods
326 (secondReductionCanonicalOrderedTargetHeadIndex tailLen p q ⟨1, by decide⟩ k) =
327 m₂' := by
328 let L := secondReductionCanonicalOrderedTargetBlockLen tailLen p
329 have hpos : (p - 2) + p * tailLen + (1 : ℕ) < L := by
330 dsimp [L, secondReductionCanonicalOrderedTargetBlockLen]
331 omega
332 have hmod :
333 (2 + k.val * L + ((p - 2) + p * tailLen + (1 : ℕ)) - 2) % L =
334 (p - 2) + p * tailLen + 1 := by
335 have hsub :
336 2 + k.val * L + ((p - 2) + p * tailLen + (1 : ℕ)) - 2 =
337 k.val * L + ((p - 2) + p * tailLen + 1) := by omega
338 rw [hsub, Nat.mul_comm k.val L, Nat.mul_add_mod_self_left, Nat.mod_eq_of_lt hpos]
339 have hnot0 : ¬ 2 + k.val * L + ((p - 2) + p * tailLen + (1 : ℕ)) = 0 := by omega
340 have hnot1 : ¬ 2 + k.val * L + ((p - 2) + p * tailLen + (1 : ℕ)) = 1 := by omega
341 have hnotMid : ¬ (p - 2) + p * tailLen + 1 < p - 2 := by omega
342 have hnotTail : ¬ (p - 2) + p * tailLen + 1 < (p - 2) + p * tailLen := by omega
343 have hnotHead0 : ¬ (p - 2) + p * tailLen + 1 = (p - 2) + p * tailLen := by omega
344 have hmodActual :
345 (2 + k.val * L + (p - 2) + p * tailLen - 1) % L =
346 (p - 2) + p * tailLen + 1 := by
347 rw [show 2 + k.val * L + (p - 2) + p * tailLen - 1 =
348 2 + k.val * L + ((p - 2) + p * tailLen + 1) - 2 by omega]
349 exact hmod
350 simp only [secondReductionCanonicalOrderedTargetSignature, secondReductionCanonicalOrderedTargetHeadIndex,
351 secondReductionCanonicalOrderedTargetPeriod, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, mul_eq_zero, false_and,
352 one_ne_zero, and_self, ↓reduceDIte, Nat.add_eq_right, Nat.reduceSubDiff, hmodActual, hnotMid, hnotTail,
353 Nat.add_eq_left, L]
355 (tailLen p q : ℕ)
356 (r : Fin (q * secondReductionCanonicalOrderedTargetBlockLen tailLen p)) :
357 Fin (secondReductionCanonicalOrderedTargetNumPeriods tailLen p q) :=
358 ⟨2 + r.val, by
360 omega⟩
362 (tailLen p q : ℕ) (k : Fin q)
363 (r : Fin (secondReductionCanonicalOrderedTargetBlockLen tailLen p)) :
364 Fin (secondReductionCanonicalOrderedTargetNumPeriods tailLen p q) :=
366 ⟨k.val * secondReductionCanonicalOrderedTargetBlockLen tailLen p + r.val, by
367 let L := secondReductionCanonicalOrderedTargetBlockLen tailLen p
368 have hblock : k.val * L + r.val < (k.val + 1) * L := by
369 calc
370 k.val * L + r.val < k.val * L + L :=
371 Nat.add_lt_add_left r.isLt _
372 _ = (k.val + 1) * L := by rw [Nat.add_mul, one_mul]
373 have hle : (k.val + 1) * L ≤ q * L :=
374 Nat.mul_le_mul_right L (Nat.succ_le_of_lt k.isLt)
375 simpa [L] using lt_of_lt_of_le hblock hle⟩
376noncomputable def secondReductionCanonicalOrderedTargetZeroBlockWord
377 {tailLen p q : ℕ}
378 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
379 (hp : 2 ≤ p) (hq : 2 ≤ q)
380 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
381 (htail : ∀ j, 2 ≤ tail j) :
382 let τ :=
384 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
385 Fin q → FreeGroup (FuchsianGenerator τ) := by
386 classical
387 dsimp
388 let τ :=
390 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
391 intro k
392 exact
393 (List.ofFn (fun r : Fin (secondReductionCanonicalOrderedTargetBlockLen tailLen p) =>
394 xWord τ (secondReductionCanonicalOrderedTargetBlockIndex tailLen p q k r))).prod
395private theorem secondReduction_list_prod_ofFn_add
396 {α : Type*} [Monoid α] {m n : ℕ} (f : Fin (m + n) → α) :
397 (List.ofFn f).prod =
398 (List.ofFn (fun i : Fin m => f (Fin.castAdd n i))).prod *
399 (List.ofFn (fun j : Fin n => f (Fin.natAdd m j))).prod := by
400 rw [← List.prod_append, ← List.ofFn_fin_append]
401 congr
402 funext i
403 cases i using Fin.addCases with
404 | left a =>
405 simp only [Fin.append_left]
406 | right b =>
407 simp only [Fin.append_right]
408private theorem secondReduction_list_prod_ofFn_cast_add
409 {α : Type*} [Monoid α] {l m n : ℕ} (h : l = m + n) (f : Fin l → α) :
410 (List.ofFn f).prod =
411 (List.ofFn (fun i : Fin m => f (Fin.cast h.symm (Fin.castAdd n i)))).prod *
412 (List.ofFn (fun j : Fin n => f (Fin.cast h.symm (Fin.natAdd m j)))).prod := by
413 rw [List.ofFn_congr h f]
415 (fun i : Fin (m + n) => f (Fin.cast h.symm i))
416private theorem secondReductionCanonicalOrderedTargetBlockIndex_middleRest
417 (tailLen p q : ℕ) (k : Fin q) (r : Fin (p - 2)) :
418 secondReductionCanonicalOrderedTargetBlockIndex tailLen p q k
419 ⟨r.val, by
420 have hr := r.isLt
421 simp only [secondReductionCanonicalOrderedTargetBlockLen, gt_iff_lt]
422 omega⟩ =
423 secondReductionCanonicalOrderedTargetMiddleRestIndex tailLen p q r k := by
424 ext
425 simp only [secondReductionCanonicalOrderedTargetBlockIndex,
426 secondReductionCanonicalOrderedTargetFlatBlockIndex, secondReductionCanonicalOrderedTargetMiddleRestIndex]
427 omega
428private theorem secondReductionCanonicalOrderedTargetBlockIndex_tail
429 (tailLen p q : ℕ) (k : Fin q) (b : Fin p) (j : Fin tailLen) :
430 secondReductionCanonicalOrderedTargetBlockIndex tailLen p q k
431 ⟨(p - 2) + (b.val * tailLen + j.val), by
432 let L := secondReductionCanonicalOrderedTargetBlockLen tailLen p
433 have hbj : b.val * tailLen + j.val < p * tailLen := by
434 have hblock : b.val * tailLen + j.val < (b.val + 1) * tailLen := by
435 calc
436 b.val * tailLen + j.val < b.val * tailLen + tailLen :=
437 Nat.add_lt_add_left j.isLt _
438 _ = (b.val + 1) * tailLen := by rw [Nat.add_mul, one_mul]
439 have hle : (b.val + 1) * tailLen ≤ p * tailLen :=
440 Nat.mul_le_mul_right tailLen (Nat.succ_le_of_lt b.isLt)
441 exact lt_of_lt_of_le hblock hle
442 dsimp [L, secondReductionCanonicalOrderedTargetBlockLen]
443 omega⟩ =
444 secondReductionCanonicalOrderedTargetTailIndex tailLen p q b j k := by
445 ext
446 simp only [secondReductionCanonicalOrderedTargetBlockIndex,
447 secondReductionCanonicalOrderedTargetFlatBlockIndex, secondReductionCanonicalOrderedTargetTailIndex]
448 omega
450 {tailLen p q : ℕ}
451 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
452 (hp : 2 ≤ p) (hq : 2 ≤ q)
453 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
454 (htail : ∀ j, 2 ≤ tail j) (k : Fin q) :
455 let τ :=
457 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
459 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k =
460 (List.ofFn (fun r : Fin (p - 2) =>
461 xWord τ (secondReductionCanonicalOrderedTargetMiddleRestIndex tailLen p q r k))).prod *
462 (List.ofFn (fun b : Fin p =>
463 (List.ofFn (fun j : Fin tailLen =>
464 xWord τ (secondReductionCanonicalOrderedTargetTailIndex tailLen p q b j k))).prod)).prod *
465 xWord τ (secondReductionCanonicalOrderedTargetHeadIndex tailLen p q ⟨0, by decide⟩ k) *
466 xWord τ (secondReductionCanonicalOrderedTargetHeadIndex tailLen p q ⟨1, by decide⟩ k) := by
467 classical
468 dsimp
469 let τ :=
471 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
472 let L := secondReductionCanonicalOrderedTargetBlockLen tailLen p
473 let f : Fin L → FreeGroup (FuchsianGenerator τ) := fun r =>
474 xWord τ (secondReductionCanonicalOrderedTargetBlockIndex tailLen p q k r)
475 change (List.ofFn f).prod = _
476 have hL : L = (p - 2) + (p * tailLen + 2) := by
477 dsimp [L, secondReductionCanonicalOrderedTargetBlockLen]
478 omega
479 rw [secondReduction_list_prod_ofFn_cast_add hL f]
480 have hmiddle :
481 (List.ofFn (fun i : Fin (p - 2) =>
482 f (Fin.cast hL.symm (Fin.castAdd (p * tailLen + 2) i)))).prod =
483 (List.ofFn (fun r : Fin (p - 2) =>
484 xWord τ (secondReductionCanonicalOrderedTargetMiddleRestIndex tailLen p q r k))).prod := by
485 congr
486 funext r
487 dsimp [f]
488 congr
489 exact secondReductionCanonicalOrderedTargetBlockIndex_middleRest tailLen p q k r
490 let g : Fin (p * tailLen + 2) → FreeGroup (FuchsianGenerator τ) := fun s =>
491 f (Fin.cast hL.symm (Fin.natAdd (p - 2) s))
492 have hrest :
493 (List.ofFn (fun j : Fin (p * tailLen + 2) =>
494 f (Fin.cast hL.symm (Fin.natAdd (p - 2) j)))).prod =
495 (List.ofFn (fun b : Fin p =>
496 (List.ofFn (fun j : Fin tailLen =>
497 xWord τ (secondReductionCanonicalOrderedTargetTailIndex tailLen p q b j k))).prod)).prod *
498 xWord τ (secondReductionCanonicalOrderedTargetHeadIndex tailLen p q ⟨0, by decide⟩ k) *
499 xWord τ (secondReductionCanonicalOrderedTargetHeadIndex tailLen p q ⟨1, by decide⟩ k) := by
500 change (List.ofFn g).prod = _
502 have htailFlat :
503 (List.ofFn (fun i : Fin (p * tailLen) => g (Fin.castAdd 2 i))).prod =
504 (List.ofFn (fun b : Fin p =>
505 (List.ofFn (fun j : Fin tailLen =>
506 xWord τ (secondReductionCanonicalOrderedTargetTailIndex tailLen p q b j k))).prod)).prod := by
508 congr
509 funext b
510 congr
511 funext j
512 dsimp [g, f]
513 congr
514 exact secondReductionCanonicalOrderedTargetBlockIndex_tail tailLen p q k b j
515 have hheads :
516 (List.ofFn (fun j : Fin 2 => g (Fin.natAdd (p * tailLen) j))).prod =
517 xWord τ (secondReductionCanonicalOrderedTargetHeadIndex tailLen p q ⟨0, by decide⟩ k) *
518 xWord τ (secondReductionCanonicalOrderedTargetHeadIndex tailLen p q ⟨1, by decide⟩ k) := by
519 rw [List.ofFn_succ]
520 rw [List.ofFn_succ]
521 have hhead :
522 ∀ h : Fin 2,
523 secondReductionCanonicalOrderedTargetBlockIndex tailLen p q k
524 (Fin.cast hL.symm (Fin.natAdd (p - 2) (Fin.natAdd (p * tailLen) h))) =
525 secondReductionCanonicalOrderedTargetHeadIndex tailLen p q h k := by
526 intro h
527 ext
528 simp only [secondReductionCanonicalOrderedTargetBlockIndex,
529 secondReductionCanonicalOrderedTargetFlatBlockIndex, secondReductionCanonicalOrderedTargetBlockLen, Fin.val_cast,
530 Fin.val_natAdd, secondReductionCanonicalOrderedTargetHeadIndex, L]
531 omega
532 simp only [Fin.isValue, hhead, Fin.succ_zero_eq_one, List.ofFn_zero, List.prod_cons, List.prod_nil, mul_one,
533 Fin.zero_eta, Fin.mk_one, g, f]
534 rw [htailFlat, hheads]
535 simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, mul_assoc]
536 rw [hmiddle, hrest]
537 simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, mul_assoc, τ]
539 {tailLen p q : ℕ}
540 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
541 (hp : 2 ≤ p) (hq : 2 ≤ q)
542 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
543 (htail : ∀ j, 2 ≤ tail j) :
544 let τ :=
546 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
547 let A :=
548 xWord τ (secondReductionCanonicalOrderedTargetDistinguishedIndex tailLen p q
549 ⟨0, by decide⟩)
550 let B :=
551 xWord τ (secondReductionCanonicalOrderedTargetDistinguishedIndex tailLen p q
552 ⟨1, by decide⟩)
553 let C :=
554 (List.ofFn (fun k : Fin q =>
556 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k)).prod
557 totalRelation τ = A * B * C := by
558 classical
559 let τ :=
561 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
562 let L := secondReductionCanonicalOrderedTargetBlockLen tailLen p
563 let flat :=
564 (List.ofFn (fun r : Fin (q * L) =>
565 xWord τ (secondReductionCanonicalOrderedTargetFlatBlockIndex tailLen p q r))).prod
566 let blocks :=
567 (List.ofFn (fun k : Fin q =>
569 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k)).prod
570 have hflat_blocks : flat = blocks := by
571 dsimp [flat, blocks, secondReductionCanonicalOrderedTargetZeroBlockWord]
573 congr
574 have htwo :
575 totalRelation τ =
576 xWord τ (secondReductionCanonicalOrderedTargetDistinguishedIndex tailLen p q
577 ⟨0, by decide⟩) *
578 xWord τ (secondReductionCanonicalOrderedTargetDistinguishedIndex tailLen p q
579 ⟨1, by decide⟩) *
580 flat := by
581 rw [totalRelation]
582 simpa [τ, flat, L, secondReductionCanonicalOrderedTargetSignature,
584 secondReductionCanonicalOrderedTargetFlatBlockIndex, List.ofFn_eq_map,
585 List.prod_cons, mul_assoc] using
586 congrArg List.prod
589 simpa [τ, blocks, flat, hflat_blocks, mul_assoc] using htwo
590end FenchelNielsen