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

FenchelNielsenZomorrodian/Discrete/CompactFuchsian/ZeroGenus/Reductions.lean

1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.ZeroGenus.Reindexing
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/ZeroGenus/Reductions.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Compact zero-genus three-step proof data
14Organizes first and second reduction data, perfectness numerics, reindexing, cleanup data, and the final zero-genus three-step finite-index theorem.
15-/
17namespace FenchelNielsen
20 q : ℕ
21 hqPrime : q.Prime
22 k : Fin D.tailLen
23 hqk : q ∣ D.tail k
24 hm₃pos : 0 < D.tail k / q
25noncomputable def FirstReductionPeriodData.tailPrimeDivisorData
28 classical
29 let k : Fin D.tailLen := ⟨0, D.hTailLen⟩
30 have htail_ge : 2 ≤ D.tail k := D.htail k
31 have htail_pos : 0 < D.tail k := lt_of_lt_of_le (by decide : 0 < 2) htail_ge
32 have htail_ne_one : D.tail k ≠ 1 := by omega
33 let hqExists : ∃ q, q.Prime ∧ q ∣ D.tail k := Nat.exists_prime_and_dvd htail_ne_one
34 let q := Classical.choose hqExists
35 have hqPrime : q.Prime := (Classical.choose_spec hqExists).1
36 have hqk : q ∣ D.tail k := (Classical.choose_spec hqExists).2
37 exact
38 { q := q
39 hqPrime := hqPrime
40 k := k
41 hqk := hqk
42 hm₃pos := Nat.div_pos (Nat.le_of_dvd htail_pos hqk) hqPrime.pos }
45 (secondPrime : FirstKernelTailPrimeDivisorData D) where
46 tailLen : ℕ
47 m₃' : ℕ
48 tail : Fin tailLen → ℕ
49 hm₃' : 0 < m₃'
50 htail : ∀ j, 2 ≤ tail j
51 reindexTail : Fin (tailLen + 1) ≃ Fin D.tailLen
52 tail_eq :
53 ∀ j, firstReductionTailIncludingThird (q := secondPrime.q) m₃' tail j =
54 D.tail (reindexTail j)
58 SecondStageCleanupPeriodData D secondPrime := by
59 classical
60 let tailLen := D.tailLen - 1
61 have hLen : tailLen + 1 = D.tailLen := by
62 have hpos : 1 ≤ D.tailLen := Nat.succ_le_of_lt D.hTailLen
63 omega
64 let k' : Fin (tailLen + 1) := (finCongr hLen).symm secondPrime.k
65 let reindexTail : Fin (tailLen + 1) ≃ Fin D.tailLen :=
66 (finHeadInsertionEquiv k').trans (finCongr hLen)
67 let tail : Fin tailLen → ℕ := fun j => D.tail (reindexTail j.succ)
68 have hmul : secondPrime.q * (D.tail secondPrime.k / secondPrime.q) =
69 D.tail secondPrime.k := by
70 rw [Nat.mul_comm]
71 exact Nat.div_mul_cancel secondPrime.hqk
72 exact
73 { tailLen := tailLen
74 m₃' := D.tail secondPrime.k / secondPrime.q
75 tail := tail
76 hm₃' := secondPrime.hm₃pos
77 htail := by
78 intro j
79 exact D.htail (reindexTail j.succ)
80 reindexTail := reindexTail
81 tail_eq := by
82 intro j
83 refine Fin.cases ?_ ?_ j
84 · change secondPrime.q * (D.tail secondPrime.k / secondPrime.q) =
85 D.tail (reindexTail 0)
86 simpa [reindexTail, k'] using hmul
87 · intro a
88 rfl }
89noncomputable def SecondStageCleanupPeriodData.reindexSource
92 (E : SecondStageCleanupPeriodData D secondPrime) :
94 Equiv.sumCongr (Equiv.refl (Fin 2)) E.reindexTail
95noncomputable def SecondStageCleanupPeriodData.sourceSignature
98 (E : SecondStageCleanupPeriodData D secondPrime) :
101 (firstReductionTailIncludingThird (q := secondPrime.q) E.m₃' E.tail)
102 D.hp D.hm₁' D.hm₂'
104 secondPrime.hqPrime.two_le E.m₃' E.tail E.hm₃' E.htail)
105 (Nat.succ_pos _)
109 (E : SecondStageCleanupPeriodData D secondPrime) :
110 Nonempty (FuchsianPresentedGroup D.sourceSignature ≃*
111 FuchsianPresentedGroup E.sourceSignature) := by
112 refine
113 zeroGenusFuchsianPresentedGroupEquivOfIndexedPeriods D.sourceSignature E.sourceSignature
114 ?_ ?_
115 (E.reindexSource.trans (originalFirstReductionOrderedIndexEquiv D.tailLen))
117 · rfl
118 · rfl
119 · intro x
120 cases x using Sum.casesOn with
121 | inl i =>
122 fin_cases i <;>
123 rfl
124 | inr j =>
125 have hD : 2 + (E.reindexTail j).val ≠ 1 := by omega
126 have hE : 2 + j.val ≠ 1 := by omega
127 simpa [SecondStageCleanupPeriodData.sourceSignature,
128 FirstReductionPeriodData.sourceSignature, originalFirstReductionSignature,
130 originalFirstReductionPeriods, twoPeriods, SecondStageCleanupPeriodData.reindexSource,
131 hD, hE]
132 using (E.tail_eq j).symm
134theorem SecondStageCleanupPeriodData.source_nonOne_periods_ge_two
137 (E : SecondStageCleanupPeriodData D secondPrime) :
139 (secondReductionSourcePeriods (p := D.p) (q := secondPrime.q)
140 D.m₁' D.m₂' E.m₃' E.tail),
142 (secondReductionSourcePeriods (p := D.p) (q := secondPrime.q)
143 D.m₁' D.m₂' E.m₃' E.tail) i :=
145 secondPrime.hqPrime.two_le D.m₁' D.m₂' E.m₃' E.tail
146 D.hm₁' D.hm₂' E.hm₃'
147 (fun j => lt_of_lt_of_le (by decide : 0 < 2) (E.htail j))
149theorem SecondStageCleanupPeriodData.source_nonOne_card_ge_three_of_firstHead
152 (E : SecondStageCleanupPeriodData D secondPrime)
153 (hm₁ne : D.m₁' ≠ 1) :
154 3 ≤ Fintype.card
156 (secondReductionSourcePeriods (p := D.p) (q := secondPrime.q)
157 D.m₁' D.m₂' E.m₃' E.tail)) := by
158 let periods :=
159 secondReductionSourcePeriods (p := D.p) (q := secondPrime.q)
160 D.m₁' D.m₂' E.m₃' E.tail
161 have hqm_ne : secondPrime.q * E.m₃' ≠ 1 := by
162 have hqge : 2 ≤ secondPrime.q * E.m₃' :=
163 le_trans secondPrime.hqPrime.two_le
164 (Nat.le_mul_of_pos_right secondPrime.q E.hm₃')
165 omega
166 let f : Fin 3 → NonOneSubfamilyIndex periods := fun i =>
167 match i with
168 | ⟨0, _⟩ =>
169 ⟨.inl 0, by
170 simpa [periods, secondReductionSourcePeriods, twoPeriods] using hm₁ne⟩
171 | ⟨1, _⟩ =>
172 ⟨.inr (.inl 0), by
173 simpa [periods, secondReductionSourcePeriods] using hqm_ne⟩
174 | ⟨2, _⟩ =>
175 ⟨.inr (.inl 1), by
176 simpa [periods, secondReductionSourcePeriods] using hqm_ne⟩
177 | ⟨n + 3, hn⟩ => False.elim (by omega)
178 have hf : Function.Injective f := by
179 intro a b h
180 fin_cases a <;> fin_cases b <;> first | rfl | cases h
181 simpa using Fintype.card_le_of_injective f hf
183end FenchelNielsen