FenchelNielsenZomorrodian/Discrete/CompactFuchsian/PeriodFamilies.lean
1import FenchelNielsenZomorrodian.Discrete.Singerman.KernelTransport
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/PeriodFamilies.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 Fuchsian proof infrastructure
14Presentation-level compact Fuchsian period families and quotient constructions used in the FNZ profinite bridge.
15-/
17namespace FenchelNielsen
19def twoPeriods {α : Type*} (a b : α) : Fin 2 → α :=
20 Fin.cases a (fun _ => b)
21@[simp 900] theorem twoPeriods_zero {α : Type*} (a b : α) :
22 twoPeriods a b 0 = a := rfl
23@[simp 900] theorem twoPeriods_one {α : Type*} (a b : α) :
24 twoPeriods a b 1 = b := rfl
25@[simp 900] theorem fin_cases_const_one {α : Type*} (a b : α) :
26 Fin.cases a (fun _ : Fin 1 => b) 1 = b := rfl
27abbrev OriginalFirstReductionIndex (tailLen : ℕ) := Sum (Fin 2) (Fin tailLen)
28def originalFirstReductionPeriods {tailLen p : ℕ}
29 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) :
30 OriginalFirstReductionIndex tailLen → ℕ
31 | .inl i => twoPeriods (p * m₁') (p * m₂') i
32 | .inr j => tail j
33abbrev FirstReductionIndex (tailLen p : ℕ) := Sum (Fin 2) (Fin tailLen × Fin p)
34def firstReductionPeriods {tailLen p : ℕ}
35 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) :
36 FirstReductionIndex tailLen p → ℕ
37 | .inl i => twoPeriods m₁' m₂' i
38 | .inr jk => tail jk.1
39abbrev FirstSecondInputIndex (tailLen p : ℕ) := Sum (Fin 2) (Sum (Fin p) (Fin tailLen × Fin p))
40abbrev SecondReductionSourceIndex (tailLen p : ℕ) :=
41 Sum (Fin 2) (Sum (Fin 2) (Sum (Fin (p - 2)) (Fin tailLen × Fin p)))
42def secondReductionSourcePeriods {tailLen p q : ℕ}
43 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ) :
44 SecondReductionSourceIndex tailLen p → ℕ
45 | .inl i => twoPeriods m₁' m₂' i
46 | .inr (.inl _) => q * m₃'
47 | .inr (.inr (.inl _)) => q * m₃'
48 | .inr (.inr (.inr jk)) => tail jk.1
49def secondReductionSourceCycleCount {tailLen p q : ℕ} :
50 SecondReductionSourceIndex tailLen p → ℕ
51 | .inl _ => q
52 | .inr (.inl _) => 1
53 | .inr (.inr (.inl _)) => q
54 | .inr (.inr (.inr _)) => q
55def secondReductionSourceTransportPeriods {tailLen p q : ℕ}
56 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ) :
57 ∀ i : SecondReductionSourceIndex tailLen p,
58 Fin (secondReductionSourceCycleCount (q := q) i) → ℕ
59 | .inl i, _ => twoPeriods m₁' m₂' i
60 | .inr (.inl _), _ => m₃'
61 | .inr (.inr (.inl _)), _ => q * m₃'
62 | .inr (.inr (.inr jk)), _ => tail jk.1
63abbrev SecondReductionTransportIndex (tailLen p q : ℕ) :=
64 Σ i : SecondReductionSourceIndex tailLen p,
65 Fin (secondReductionSourceCycleCount (tailLen := tailLen) (p := p) (q := q) i)
66abbrev secondReductionTransportPeriods {tailLen p q : ℕ}
67 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ) :
68 SecondReductionTransportIndex tailLen p q → ℕ :=
70 (secondReductionSourceTransportPeriods (p := p) (q := q) m₁' m₂' m₃' tail)
72 {tailLen p q : ℕ} (hq : 2 ≤ q)
73 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ) :
74 HasEqualPartnerFamily (secondReductionTransportPeriods (p := p) (q := q) m₁' m₂' m₃' tail) := by
75 intro x
76 rcases x with ⟨i, k⟩
77 cases i with
78 | inl i =>
79 refine ⟨⟨.inl i, finPartner hq k⟩, ?_, ?_⟩
80 · intro h
81 have hk : finPartner hq k = k := by
82 simpa using eq_of_heq (Sigma.mk.inj_iff.mp h).2
83 exact finPartner_ne hq k hk
84 · rfl
85 | inr s =>
86 cases s with
87 | inl j =>
88 refine ⟨⟨.inr (.inl (finPartner (by decide : 2 ≤ 2) j)),
89 by simpa [secondReductionSourceCycleCount] using (0 : Fin 1)⟩, ?_, ?_⟩
90 · intro h
91 have hj : finPartner (by decide : 2 ≤ 2) j = j := by
92 simpa using (Sigma.mk.inj_iff.mp h).1
93 exact finPartner_ne (by decide : 2 ≤ 2) j hj
94 · rfl
95 | inr s =>
96 cases s with
97 | inl j =>
98 refine ⟨⟨.inr (.inr (.inl j)), finPartner hq k⟩, ?_, ?_⟩
99 · intro h
100 have hk : finPartner hq k = k := by
101 simpa using eq_of_heq (Sigma.mk.inj_iff.mp h).2
102 exact finPartner_ne hq k hk
103 · rfl
104 | inr jk =>
105 refine ⟨⟨.inr (.inr (.inr jk)), finPartner hq k⟩, ?_, ?_⟩
106 · intro h
107 have hk : finPartner hq k = k := by
108 simpa using eq_of_heq (Sigma.mk.inj_iff.mp h).2
109 exact finPartner_ne hq k hk
110 · rfl
112end FenchelNielsen