FenchelNielsenZomorrodian/Discrete/CompactFuchsian/PeriodOne/TargetSignatures.lean
1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.FirstReduction.Signatures
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/PeriodOne/TargetSignatures.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
14Handles the cleanup of period-one target entries using quotient maps, kernel equivalences, low-cardinality dihedral cases, source subgroups, and relator proofs.
15-/
17open scoped BigOperators
18namespace FenchelNielsen
20noncomputable def doublePeriodOneTailReplicatedSignature
21 {tailLen p : ℕ} (tail : Fin tailLen → ℕ)
22 (htail : ∀ j, 2 ≤ tail j) (hHigh : 3 ≤ p * tailLen) :
23 FuchsianSignature where
24 orbitGenus := 0
25 numCusps := 0
26 numPeriods := p * tailLen
27 periods := fun i => tail ((finProdFinEquiv.symm i).2)
28 period_ge_two := by
29 intro i
30 exact htail ((finProdFinEquiv.symm i).2)
31 numCusps_eq_zero := rfl
32 numPeriods_ge_three := hHigh
35 {tailLen p : ℕ} (tail : Fin tailLen → ℕ)
36 (htail : ∀ j, 2 ≤ tail j) (hHigh : 3 ≤ p * tailLen) :
37 2 ≤ p →
39 (doublePeriodOneTailReplicatedSignature tail htail hHigh).toFenchelSignature := by
40 classical
41 intro hp
42 change LCMConditionFamily
43 (fun i : Fin (p * tailLen) => tail ((finProdFinEquiv.symm i).2))
45 intro i
46 let kj : Fin p × Fin tailLen := finProdFinEquiv.symm i
47 refine ⟨finProdFinEquiv (finPartner hp kj.1, kj.2), ?_, ?_⟩
48 · intro h
49 have hi : i = finProdFinEquiv kj := by
50 dsimp [kj]
51 exact (finProdFinEquiv.apply_symm_apply i).symm
52 have hpair := finProdFinEquiv.injective (h.trans hi)
53 exact finPartner_ne hp kj.1 (congrArg Prod.fst hpair)
54 · simp only [finProdFinEquiv_symm_apply, Equiv.symm_apply_apply, kj]
56abbrev OneHeadPeriodOneTargetIndex (tailLen p : ℕ) :=
57 Sum (Fin 1) (Fin p × Fin tailLen)
59def oneHeadPeriodOneTargetOrderedIndexEquiv (tailLen p : ℕ) :
60 OneHeadPeriodOneTargetIndex tailLen p ≃ Fin (1 + p * tailLen) :=
61 (Equiv.sumCongr (Equiv.refl (Fin 1))
62 (finProdFinEquiv : Fin p × Fin tailLen ≃ Fin (p * tailLen))).trans
63 finSumFinEquiv
66 {tailLen p : ℕ} (m₂' : ℕ) (tail : Fin tailLen → ℕ) :
67 OneHeadPeriodOneTargetIndex tailLen p → ℕ
68 | .inl _ => m₂'
69 | .inr kj => tail kj.2
71noncomputable def oneHeadPeriodOneTargetSignature
72 {tailLen p : ℕ} (m₂' : ℕ) (tail : Fin tailLen → ℕ)
73 (hp : 2 ≤ p) (hm₂' : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j)
74 (hTailLen : 0 < tailLen) : FuchsianSignature where
75 orbitGenus := 0
76 numCusps := 0
77 numPeriods := 1 + p * tailLen
78 periods := fun i =>
79 oneHeadPeriodOneTargetPeriods (p := p) m₂' tail
80 ((oneHeadPeriodOneTargetOrderedIndexEquiv tailLen p).symm i)
81 period_ge_two := by
82 intro i
83 cases h :
84 (oneHeadPeriodOneTargetOrderedIndexEquiv tailLen p).symm i with
85 | inl head =>
86 fin_cases head
87 exact hm₂'
88 | inr kj =>
89 exact htail kj.2
90 numCusps_eq_zero := rfl
91 numPeriods_ge_three := by
92 have htailOne : 1 ≤ tailLen := Nat.succ_le_of_lt hTailLen
93 have hprod : 2 ≤ p * tailLen := by
94 exact Nat.mul_le_mul hp htailOne
95 omega
97end FenchelNielsen