FenchelNielsenZomorrodian/Discrete/Core/Signature.lean
1import FenchelNielsenZomorrodian.Discrete.Arithmetic.FamilyLcm
2import Mathlib.Tactic.Linarith
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Core/Signature.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Discrete Fenchel and compact Fuchsian core definitions
15Signatures, generator indices, presentations, elliptic generators, quotient homomorphisms, and family-signature transformations.
16-/
18open scoped BigOperators
20namespace FenchelNielsen
22structure FenchelSignature where
23 orbitGenus : ℕ
24 numCusps : ℕ
25 numPeriods : ℕ
26 periods : Fin numPeriods → ℕ
27 period_ge_two : ∀ i, 2 ≤ periods i
29def FenchelSignature.eulerCharacteristic (σ : FenchelSignature) : ℚ :=
30 (2 : ℚ) - 2 * σ.orbitGenus - σ.numCusps -
31 ∑ i : Fin σ.numPeriods, (1 - ((σ.periods i : ℚ)⁻¹))
33def FenchelSignature.hyperbolicDefect (σ : FenchelSignature) : ℚ :=
34 -(σ.eulerCharacteristic)
36def FenchelSignature.IsHyperbolic (σ : FenchelSignature) : Prop :=
37 σ.eulerCharacteristic < 0
39theorem FenchelSignature.isHyperbolic_iff_pos_hyperbolicDefect
40 {σ : FenchelSignature} :
41 σ.IsHyperbolic ↔ 0 < σ.hyperbolicDefect := by
42 dsimp [FenchelSignature.IsHyperbolic, FenchelSignature.hyperbolicDefect]
43 constructor <;> intro h <;> linarith
45def FenchelSignature.HasCusps (σ : FenchelSignature) : Prop :=
46 0 < σ.numCusps
48def FenchelSignature.IsCompact (σ : FenchelSignature) : Prop :=
49 σ.numCusps = 0
52def otherPeriodsLcm (σ : FenchelSignature) (i : Fin σ.numPeriods) : ℕ :=
53 otherPeriodsLcmFamily σ.periods i
55def otherPeriodsProduct (σ : FenchelSignature) (i : Fin σ.numPeriods) : ℕ :=
56 otherPeriodsProductFamily σ.periods i
58def LCMCondition (σ : FenchelSignature) : Prop :=
59 LCMConditionFamily σ.periods
61def FenchelSignature.AbelianPeriodCondition (σ : FenchelSignature) : Prop :=
65 (σ : FenchelSignature) (hNotLCM : ¬ LCMCondition σ) :
66 ∃ i : Fin σ.numPeriods, ¬ σ.periods i ∣ otherPeriodsLcm σ i := by
67 classical
68 simpa [LCMCondition, LCMConditionFamily, otherPeriodsLcm] using
69 not_forall.mp hNotLCM
71end FenchelNielsen