FenchelNielsenZomorrodian/Discrete/CompactFuchsian/FirstReduction/Signatures.lean
1import FenchelNielsenZomorrodian.Discrete.Singerman.FreeGroupWords
2import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.ZeroGenus.FirstReductionData
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/FirstReduction/Signatures.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
15The first explicit finite quotient reduction for compact zero-genus Fuchsian presentations, including quotient maps, basis transport, signatures, and relator verification.
16-/
18namespace FenchelNielsen
19noncomputable abbrev firstReductionSourceSignature
20 {tailLen p : ℕ}
21 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
22 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
23 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
25 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
27theorem list_prod_ofFn_mul_blocks {α : Type*} [Monoid α] {p n : ℕ}
28 (f : Fin (p * n) → α) :
29 (List.ofFn f).prod =
30 (List.ofFn (fun k : Fin p =>
31 (List.ofFn (fun j : Fin n =>
32 f ⟨k.val * n + j.val, by
33 calc
34 k.val * n + j.val < (k.val + 1) * n := by
35 calc
36 k.val * n + j.val < k.val * n + n :=
37 Nat.add_lt_add_left j.isLt _
38 _ = (k.val + 1) * n := by rw [Nat.add_mul, one_mul]
39 _ ≤ p * n := Nat.mul_le_mul_right n (Nat.succ_le_of_lt k.isLt)⟩)).prod)).prod := by
40 rw [List.ofFn_mul]
41 rw [List.prod_flatten]
42 rw [List.map_ofFn]
43 congr
45 {tailLen p : ℕ}
46 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) (i : Fin (2 + tailLen)) : ℕ :=
47 if h0 : i.val = 0 then
48 p * m₁'
49 else if h1 : i.val = 1 then
50 p * m₂'
51 else
52 tail ⟨i.val - 2, by omega⟩
53@[local simp]
55 {tailLen p : ℕ}
56 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) :
57 firstReductionCanonicalSourcePeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
58 ⟨0, by omega⟩ = p * m₁' := by
59 simp only [firstReductionCanonicalSourcePeriod, ↓reduceDIte]
60@[local simp]
62 {tailLen p : ℕ}
63 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) :
64 firstReductionCanonicalSourcePeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
65 ⟨1, by omega⟩ = p * m₂' := by
66 simp only [firstReductionCanonicalSourcePeriod, one_ne_zero, ↓reduceDIte]
67@[local simp]
69 {tailLen p : ℕ}
70 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) (j : Fin tailLen) :
71 firstReductionCanonicalSourcePeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
72 ⟨2 + j.val, by omega⟩ = tail j := by
74 have h0 : 2 + j.val ≠ 0 := by omega
75 have h1 : 2 + j.val ≠ 1 := by omega
76 simp only [Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and, ↓reduceDIte, h1, add_tsub_cancel_left,
77 Fin.eta]
79 {tailLen p : ℕ}
80 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
81 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
82 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
83 FuchsianSignature where
84 orbitGenus := 0
85 numCusps := 0
86 numPeriods := 2 + tailLen
87 periods := firstReductionCanonicalSourcePeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
88 period_ge_two := by
89 intro i
91 by_cases h0 : i.val = 0
92 · rw [dif_pos h0]
93 exact le_trans hp (Nat.le_mul_of_pos_right p (lt_of_lt_of_le (by decide) hm₁'))
94 · by_cases h1 : i.val = 1
95 · rw [dif_neg h0, dif_pos h1]
96 exact le_trans hp (Nat.le_mul_of_pos_right p (lt_of_lt_of_le (by decide) hm₂'))
97 · rw [dif_neg h0, dif_neg h1]
98 exact htail ⟨i.val - 2, by omega⟩
99 numCusps_eq_zero := rfl
100 numPeriods_ge_three := by omega
102 {tailLen p : ℕ}
103 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
104 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
105 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
106 Fin
108 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).numPeriods :=
109 ⟨0, by simp only [firstReductionCanonicalSourceSignature, add_pos_iff, Nat.ofNat_pos, true_or]⟩
111 {tailLen p : ℕ}
112 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
113 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
114 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
115 Fin
117 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).numPeriods :=
118 ⟨1, by simp only [firstReductionCanonicalSourceSignature]; omega⟩
120 {tailLen p : ℕ}
121 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
122 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
123 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) (j : Fin tailLen) :
124 Fin
126 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).numPeriods :=
127 ⟨2 + j.val, by
128 simp only [firstReductionCanonicalSourceSignature, add_lt_add_iff_left, Fin.is_lt]⟩
129@[simp 900] theorem firstReductionCanonicalSourceSignature_period_zero
130 {tailLen p : ℕ}
131 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
132 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
133 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
135 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
137 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) =
138 p * m₁' := by
139 simp only [firstReductionCanonicalSourceSignature, firstReductionCanonicalSourceZeroIndex, Fin.mk_zero',
140 firstReductionCanonicalSourcePeriod, Fin.coe_ofNat_eq_mod, Nat.zero_mod, ↓reduceDIte]
141@[simp 900] theorem firstReductionCanonicalSourceSignature_period_one
142 {tailLen p : ℕ}
143 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
144 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
145 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
147 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
149 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) =
150 p * m₂' := by
152 firstReductionCanonicalSourcePeriod, one_ne_zero, ↓reduceDIte]
153@[simp 900] theorem firstReductionCanonicalSourceSignature_period_tail
154 {tailLen p : ℕ}
155 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
156 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
157 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) (j : Fin tailLen) :
159 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
161 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j) =
162 tail j := by
166 {tailLen p : ℕ}
167 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
168 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
169 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
170 let σ :=
171 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
172 totalRelation σ =
175 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
178 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
179 (List.ofFn (fun j : Fin tailLen =>
182 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j))).prod := by
183 classical
184 let σ :=
185 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
186 change totalRelation σ =
189 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
192 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
193 (List.ofFn (fun j : Fin tailLen =>
196 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j))).prod
197 rw [totalRelation]
200 List.ofFn_eq_map, List.prod_cons, mul_assoc] using
201 congrArg List.prod
202 (list_ofFn_two_add (fun i : Fin (2 + tailLen) => xWord σ i))
204 {tailLen p : ℕ}
205 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) (hTailLen : 0 < tailLen)
206 (i : Fin (2 + p * tailLen)) : ℕ :=
207 if i.val = 0 then
208 m₁'
209 else if i.val = 1 then
210 m₂'
211 else
212 tail ⟨(i.val - 2) % tailLen, Nat.mod_lt _ hTailLen⟩
213@[local simp]
215 {tailLen p : ℕ}
216 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) (hTailLen : 0 < tailLen) :
217 firstReductionCanonicalTargetPeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
218 hTailLen ⟨0, by omega⟩ = m₁' := by
219 simp only [firstReductionCanonicalTargetPeriod, ↓reduceIte]
220@[local simp]
222 {tailLen p : ℕ}
223 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) (hTailLen : 0 < tailLen) :
224 firstReductionCanonicalTargetPeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
225 hTailLen ⟨1, by omega⟩ = m₂' := by
226 simp only [firstReductionCanonicalTargetPeriod, one_ne_zero, ↓reduceIte]
227@[local simp]
229 {tailLen p : ℕ}
230 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) (hTailLen : 0 < tailLen)
231 (k : Fin p) (j : Fin tailLen) :
232 firstReductionCanonicalTargetPeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
233 hTailLen
234 ⟨2 + k.val * tailLen + j.val, by
235 have hblock : k.val * tailLen + j.val < (k.val + 1) * tailLen := by
236 calc
237 k.val * tailLen + j.val < k.val * tailLen + tailLen :=
238 Nat.add_lt_add_left j.isLt _
239 _ = (k.val + 1) * tailLen := by rw [Nat.add_mul, one_mul]
240 have hle : (k.val + 1) * tailLen ≤ p * tailLen :=
241 Nat.mul_le_mul_right tailLen (Nat.succ_le_of_lt k.isLt)
242 have hmain : k.val * tailLen + j.val < p * tailLen :=
243 lt_of_lt_of_le hblock hle
244 omega⟩ = tail j := by
246 have h0 : 2 + k.val * tailLen + j.val ≠ 0 := by omega
247 have h1 : 2 + k.val * tailLen + j.val ≠ 1 := by omega
248 rw [if_neg h0, if_neg h1]
249 have hsub :
250 2 + k.val * tailLen + j.val - 2 = k.val * tailLen + j.val := by
251 omega
252 have hmod : (2 + k.val * tailLen + j.val - 2) % tailLen = j.val := by
253 rw [hsub, Nat.mul_comm k.val tailLen, Nat.mul_add_mod_self_left,
254 Nat.mod_eq_of_lt j.isLt]
255 exact congrArg tail (Fin.ext hmod)
257 {tailLen p : ℕ}
258 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
259 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
260 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
261 FuchsianSignature where
262 orbitGenus := 0
263 numCusps := 0
264 numPeriods := 2 + p * tailLen
265 periods :=
266 firstReductionCanonicalTargetPeriod (tailLen := tailLen) (p := p) m₁' m₂' tail hTailLen
267 period_ge_two := by
268 intro i
270 by_cases h0 : i.val = 0
271 · rw [if_pos h0]
272 exact hm₁'
273 · by_cases h1 : i.val = 1
274 · rw [if_neg h0, if_pos h1]
275 exact hm₂'
276 · rw [if_neg h0, if_neg h1]
277 exact htail ⟨(i.val - 2) % tailLen, Nat.mod_lt _ hTailLen⟩
278 numCusps_eq_zero := rfl
279 numPeriods_ge_three := by
280 have hp_pos : 0 < p := lt_of_lt_of_le (by decide : 0 < 2) hp
281 nlinarith [Nat.mul_pos hp_pos hTailLen]
283 {tailLen p : ℕ}
284 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
285 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
286 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
287 Fin
289 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).numPeriods :=
290 ⟨0, by simp only [firstReductionCanonicalTargetSignature, add_pos_iff, Nat.ofNat_pos, CanonicallyOrderedAdd.mul_pos,
291 true_or]⟩
293 {tailLen p : ℕ}
294 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
295 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
296 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
297 Fin
299 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).numPeriods :=
300 ⟨1, by
301 have hp_pos : 0 < p := lt_of_lt_of_le (by decide : 0 < 2) hp
302 have hprod : 0 < p * tailLen := Nat.mul_pos hp_pos hTailLen
303 simp only [firstReductionCanonicalTargetSignature, gt_iff_lt]
304 omega⟩
306 {tailLen p : ℕ}
307 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
308 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
309 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
310 (r : Fin (p * tailLen)) :
311 Fin
313 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).numPeriods :=
314 ⟨2 + r.val, by
315 simp only [firstReductionCanonicalTargetSignature, add_lt_add_iff_left, Fin.is_lt]⟩
316@[local simp]
318 {tailLen p : ℕ}
319 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
320 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
321 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
322 (r : Fin (p * tailLen)) :
324 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
326 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen r) =
327 tail ⟨r.val % tailLen, Nat.mod_lt _ hTailLen⟩ := by
328 change
329 firstReductionCanonicalTargetPeriod (tailLen := tailLen) (p := p)
330 m₁' m₂' tail hTailLen ⟨2 + r.val, by simp only [add_lt_add_iff_left, Fin.is_lt]⟩ =
331 tail ⟨r.val % tailLen, Nat.mod_lt _ hTailLen⟩
333 have h0 : 2 + r.val ≠ 0 := by omega
334 have h1 : 2 + r.val ≠ 1 := by omega
335 rw [if_neg h0, if_neg h1]
336 apply congrArg tail
337 ext
338 simp only [add_tsub_cancel_left]
340 {tailLen p : ℕ}
341 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
342 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
343 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
344 (k : Fin p) (j : Fin tailLen) :
345 Fin
347 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).numPeriods :=
348 ⟨2 + k.val * tailLen + j.val, by
349 have hblock : k.val * tailLen + j.val < (k.val + 1) * tailLen := by
350 calc
351 k.val * tailLen + j.val < k.val * tailLen + tailLen :=
352 Nat.add_lt_add_left j.isLt _
353 _ = (k.val + 1) * tailLen := by rw [Nat.add_mul, one_mul]
354 have hle : (k.val + 1) * tailLen ≤ p * tailLen :=
355 Nat.mul_le_mul_right tailLen (Nat.succ_le_of_lt k.isLt)
356 have hmain : k.val * tailLen + j.val < p * tailLen :=
357 lt_of_lt_of_le hblock hle
358 simp only [firstReductionCanonicalTargetSignature, gt_iff_lt]
359 omega⟩
361 {tailLen p : ℕ}
362 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
363 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
364 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
365 (i :
366 Fin
368 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).numPeriods)
369 (h0 : i.val ≠ 0) (h1 : i.val ≠ 1) :
370 let r : Fin (p * tailLen) := ⟨i.val - 2, by
371 have hi : i.val < 2 + p * tailLen := by
372 simp only [firstReductionCanonicalTargetSignature] at i
373 exact i.isLt
374 omega⟩
375 let k : Fin p := ⟨r.val / tailLen, by
376 exact Nat.div_lt_of_lt_mul (by simpa [Nat.mul_comm] using r.isLt)⟩
377 let j : Fin tailLen := ⟨r.val % tailLen, Nat.mod_lt _ hTailLen⟩
378 i =
380 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j := by
381 dsimp
382 ext
383 change i.val = 2 + (i.val - 2) / tailLen * tailLen + (i.val - 2) % tailLen
384 have hige2 : 2 ≤ i.val := by omega
385 have hdecomp :
386 (i.val - 2) / tailLen * tailLen + (i.val - 2) % tailLen = i.val - 2 :=
387 Nat.div_add_mod' (i.val - 2) tailLen
388 omega
389@[simp 900] theorem firstReductionCanonicalTargetFlatTailIndex_block
390 {tailLen p : ℕ}
391 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
392 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
393 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
394 (k : Fin p) (j : Fin tailLen) :
396 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
397 ⟨k.val * tailLen + j.val, by
398 have hblock : k.val * tailLen + j.val < (k.val + 1) * tailLen := by
399 calc
400 k.val * tailLen + j.val < k.val * tailLen + tailLen :=
401 Nat.add_lt_add_left j.isLt _
402 _ = (k.val + 1) * tailLen := by rw [Nat.add_mul, one_mul]
403 have hle : (k.val + 1) * tailLen ≤ p * tailLen :=
404 Nat.mul_le_mul_right tailLen (Nat.succ_le_of_lt k.isLt)
405 exact lt_of_lt_of_le hblock hle⟩ =
407 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j := by
408 ext
410 omega
411private theorem firstReductionCanonicalTarget_flatTailProduct_eq_blocks
412 {tailLen p : ℕ}
413 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
414 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
415 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
416 let τ :=
417 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
418 (List.ofFn (fun r : Fin (p * tailLen) =>
421 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen r))).prod =
422 (List.ofFn (fun k : Fin p =>
423 (List.ofFn (fun j : Fin tailLen =>
426 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))).prod)).prod := by
427 classical
428 let τ :=
429 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
430 change
431 (List.ofFn (fun r : Fin (p * tailLen) =>
434 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen r))).prod =
435 (List.ofFn (fun k : Fin p =>
436 (List.ofFn (fun j : Fin tailLen =>
439 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))).prod)).prod
441 congr
442 funext k
443 congr
444 funext j
446private theorem firstReductionCanonicalTarget_totalRelation_eq_flat
447 {tailLen p : ℕ}
448 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
449 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
450 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
451 let τ :=
452 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
453 totalRelation τ =
456 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
459 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
460 (List.ofFn (fun r : Fin (p * tailLen) =>
463 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen r))).prod := by
464 classical
465 let τ :=
466 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
467 change totalRelation τ =
470 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
473 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
474 (List.ofFn (fun r : Fin (p * tailLen) =>
477 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen r))).prod
478 rw [totalRelation]
481 List.ofFn_eq_map, List.prod_cons, mul_assoc] using
482 congrArg List.prod
483 (list_ofFn_two_add (fun i : Fin (2 + p * tailLen) => xWord τ i))
485 {tailLen p : ℕ}
486 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
487 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
488 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
489 let τ :=
490 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
491 totalRelation τ =
494 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
497 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
498 (List.ofFn (fun k : Fin p =>
499 (List.ofFn (fun j : Fin tailLen =>
502 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))).prod)).prod := by
503 classical
504 let τ :=
505 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
506 change totalRelation τ =
509 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
512 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
513 (List.ofFn (fun k : Fin p =>
514 (List.ofFn (fun j : Fin tailLen =>
517 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))).prod)).prod
520@[simp 900] theorem firstReductionCanonicalTargetSignature_period_zero
521 {tailLen p : ℕ}
522 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
523 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
524 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
526 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
528 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) =
529 m₁' := by
530 simp only [firstReductionCanonicalTargetSignature, firstReductionCanonicalTargetZeroIndex, Fin.mk_zero',
531 firstReductionCanonicalTargetPeriod, Fin.coe_ofNat_eq_mod, Nat.zero_mod, ↓reduceIte]
532@[simp 900] theorem firstReductionCanonicalTargetSignature_period_one
533 {tailLen p : ℕ}
534 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
535 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
536 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
538 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
540 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) =
541 m₂' := by
543 firstReductionCanonicalTargetPeriod, one_ne_zero, ↓reduceIte]
544@[simp 900] theorem firstReductionCanonicalTargetSignature_period_tail
545 {tailLen p : ℕ}
546 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
547 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
548 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
549 (k : Fin p) (j : Fin tailLen) :
551 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
553 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j) =
554 tail j := by
557end FenchelNielsen