FenchelNielsenZomorrodian/Discrete/CompactFuchsian/ZeroGenus/SecondReductionData.lean

1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.ZeroGenus.FirstReductionData

2import Mathlib.Data.Fintype.Prod

4/-

5PUBLIC_PAGE_SNAPSHOT

6generated_at: 2026-05-27T09:47:29+09:00

7lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/ZeroGenus/SecondReductionData.lean

8translation_root: data/translation

9purpose: identifies the local data snapshot used to build pages/

10placement: after imports, never before imports

11-/

12/-!

13# Compact zero-genus three-step proof data

15Organizes first and second reduction data, perfectness numerics, reindexing, cleanup data, and the final zero-genus three-step finite-index theorem.

16-/

18namespace FenchelNielsen

20noncomputable def secondReductionSourceSignature

21 {tailLen p q : ℕ}

22 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)

23 (hq : 2 ≤ q)

24 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 0 < m₃')

25 (htail : ∀ j, 2 ≤ tail j) :

26 FuchsianSignature :=

27 familyFuchsianSignature

28 (secondReductionSourcePeriods (p := p) (q := q) m₁' m₂' m₃' tail)

29 (by

30 intro i

31 cases i using Sum.casesOn <;> rename_i i

32 · fin_cases i

33 · simpa [secondReductionSourcePeriods, twoPeriods] using hm₁'

34 · simpa [secondReductionSourcePeriods, twoPeriods] using hm₂'

35 · cases i using Sum.casesOn <;> rename_i i

36 · exact le_trans hq (Nat.le_mul_of_pos_right q hm₃')

37 · cases i using Sum.casesOn <;> rename_i i

38 · exact le_trans hq (Nat.le_mul_of_pos_right q hm₃')

39 · exact htail i.1)

40 (by

41 have hcard :

42 Fintype.card (SecondReductionSourceIndex tailLen p)

43 = 2 + 2 + (p - 2) + tailLen * p := by

44 simp only [Fintype.card_sum, Fintype.card_fin, Fintype.card_prod, Nat.reduceAdd]

45 omega

46 rw [hcard]

47 omega)

49end FenchelNielsen