FenchelNielsenZomorrodian/Discrete/CompactFuchsian/ZeroGenus/FirstReductionData.lean
1import FenchelNielsenZomorrodian.Discrete.Core.FamilySignature
2import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodFamilies
3import Mathlib.Tactic.FinCases
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/ZeroGenus/FirstReductionData.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
16Organizes first and second reduction data, perfectness numerics, reindexing, cleanup data, and the final zero-genus three-step finite-index theorem.
17-/
19namespace FenchelNielsen
22 {tailLen p : ℕ}
23 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) (i : Fin (2 + tailLen)) : ℕ :=
24 if h0 : i.val = 0 then
25 p * m₁'
26 else if h1 : i.val = 1 then
27 p * m₂'
28 else
29 tail ⟨i.val - 2, by omega⟩
31@[simp 900] theorem originalFirstReductionSignaturePeriod_zero
32 {tailLen p : ℕ} (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) :
33 originalFirstReductionSignaturePeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
34 ⟨0, by omega⟩ = p * m₁' := by
35 simp only [originalFirstReductionSignaturePeriod, ↓reduceDIte]
37@[simp 900] theorem originalFirstReductionSignaturePeriod_zero_fin
38 {tailLen p : ℕ} (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) :
39 originalFirstReductionSignaturePeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
40 (0 : Fin (2 + tailLen)) = p * m₁' := by
41 rfl
43@[simp 900] theorem originalFirstReductionSignaturePeriod_one
44 {tailLen p : ℕ} (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) :
45 originalFirstReductionSignaturePeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
46 ⟨1, by omega⟩ = p * m₂' := by
47 simp only [originalFirstReductionSignaturePeriod, one_ne_zero, ↓reduceDIte]
49@[simp 900] theorem originalFirstReductionSignaturePeriod_one_fin
50 {tailLen p : ℕ} (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) :
51 originalFirstReductionSignaturePeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
52 (1 : Fin (2 + tailLen)) = p * m₂' := by
53 have hOne : (1 : Fin (2 + tailLen)) = ⟨1, by omega⟩ := by
54 apply Fin.ext
55 simp only [Fin.coe_ofNat_eq_mod]
56 rw [Nat.mod_eq_of_lt (by omega : 1 < 2 + tailLen)]
57 rw [hOne]
58 simp only [originalFirstReductionSignaturePeriod_one]
60@[simp 900] theorem originalFirstReductionSignaturePeriod_tail
61 {tailLen p : ℕ} (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) (j : Fin tailLen) :
62 originalFirstReductionSignaturePeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
63 ⟨2 + j.val, by omega⟩ = tail j := by
65 have h0 : 2 + j.val ≠ 0 := by omega
66 have h1 : 2 + j.val ≠ 1 := by omega
67 simp only [Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and, ↓reduceDIte, h1, add_tsub_cancel_left,
68 Fin.eta]
70def originalFirstReductionOrderedIndexEquiv (tailLen : ℕ) :
71 OriginalFirstReductionIndex tailLen ≃ Fin (2 + tailLen) where
72 toFun := fun
73 | .inl i => ⟨i.val, by omega⟩
74 | .inr j => ⟨2 + j.val, by omega⟩
75 invFun := fun i =>
76 if h0 : i.val = 0 then
77 .inl (0 : Fin 2)
78 else if h1 : i.val = 1 then
79 .inl (1 : Fin 2)
80 else
81 .inr ⟨i.val - 2, by omega⟩
82 left_inv := by
83 intro x
84 cases x using Sum.casesOn with
85 | inl i =>
86 fin_cases i <;> rfl
87 | inr j =>
88 simp only [Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and, ↓reduceDIte, Fin.isValue,
89 add_tsub_cancel_left, Fin.eta, dite_eq_ite, ite_eq_right_iff, reduceCtorEq, imp_false]
90 omega
91 right_inv := by
92 intro i
93 by_cases h0 : i.val = 0
94 · ext
95 simp only [h0, ↓reduceDIte, Fin.isValue, Fin.coe_ofNat_eq_mod, Nat.zero_mod, Fin.mk_zero']
96 · by_cases h1 : i.val = 1
97 · ext
98 simp only [h1, one_ne_zero, ↓reduceDIte, Fin.isValue, Fin.coe_ofNat_eq_mod, Nat.mod_succ]
99 · ext
100 simp only [h0, ↓reduceDIte, h1]
101 omega
103@[simp 900] theorem originalFirstReductionOrderedIndexEquiv_left_zero
104 (tailLen : ℕ) :
105 originalFirstReductionOrderedIndexEquiv tailLen (.inl (0 : Fin 2)) =
106 (0 : Fin (2 + tailLen)) := rfl
108@[simp 900] theorem originalFirstReductionOrderedIndexEquiv_left_one
109 (tailLen : ℕ) :
110 originalFirstReductionOrderedIndexEquiv tailLen (.inl (1 : Fin 2)) =
111 (1 : Fin (2 + tailLen)) := by
112 apply Fin.ext
113 simp only [originalFirstReductionOrderedIndexEquiv, Fin.val_eq_zero_iff, Fin.isValue, Equiv.coe_fn_mk,
114 Fin.coe_ofNat_eq_mod, Nat.mod_succ]
115 rw [Nat.mod_eq_of_lt (by omega : 1 < 2 + tailLen)]
117@[simp 900] theorem originalFirstReductionOrderedIndexEquiv_right
118 {tailLen : ℕ} (j : Fin tailLen) :
119 originalFirstReductionOrderedIndexEquiv tailLen (.inr j) =
120 ⟨2 + j.val, by omega⟩ := rfl
122@[simp 900] theorem originalFirstReductionOrderedIndexEquiv_symm_zero
123 (tailLen : ℕ) :
124 (originalFirstReductionOrderedIndexEquiv tailLen).symm (0 : Fin (2 + tailLen)) =
125 .inl (0 : Fin 2) := by
126 apply (originalFirstReductionOrderedIndexEquiv tailLen).injective
127 simp only [Equiv.apply_symm_apply, Fin.isValue, originalFirstReductionOrderedIndexEquiv_left_zero]
129@[simp 900] theorem originalFirstReductionOrderedIndexEquiv_symm_one
130 (tailLen : ℕ) :
131 (originalFirstReductionOrderedIndexEquiv tailLen).symm (1 : Fin (2 + tailLen)) =
132 .inl (1 : Fin 2) := by
133 apply (originalFirstReductionOrderedIndexEquiv tailLen).injective
134 simp only [Equiv.apply_symm_apply, Fin.isValue, originalFirstReductionOrderedIndexEquiv_left_one]
136@[simp 900] theorem originalFirstReductionOrderedIndexEquiv_symm_right
137 {tailLen : ℕ} (j : Fin tailLen) :
138 (originalFirstReductionOrderedIndexEquiv tailLen).symm ⟨2 + j.val, by omega⟩ =
139 .inr j := by
140 apply (originalFirstReductionOrderedIndexEquiv tailLen).injective
141 simp only [Equiv.apply_symm_apply, originalFirstReductionOrderedIndexEquiv_right]
143noncomputable def originalFirstReductionSignature
144 {tailLen p : ℕ}
145 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
146 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
147 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
148 FuchsianSignature where
149 orbitGenus := 0
150 numCusps := 0
151 numPeriods := 2 + tailLen
152 periods := originalFirstReductionSignaturePeriod (p := p) m₁' m₂' tail
153 period_ge_two := by
154 intro i
156 by_cases h0 : i.val = 0
157 · simp only [h0, ↓reduceDIte]
158 exact le_trans hp (Nat.le_mul_of_pos_right p hm₁')
159 · by_cases h1 : i.val = 1
160 · simp only [h1, one_ne_zero, ↓reduceDIte]
161 exact le_trans hp (Nat.le_mul_of_pos_right p hm₂')
162 · simp only [h0, ↓reduceDIte, h1]
163 exact htail ⟨i.val - 2, by omega⟩
164 numCusps_eq_zero := rfl
165 numPeriods_ge_three := by
166 omega
168end FenchelNielsen