curvature_at_identity

formal source

 115  c.value⁻¹^2 + c.value⁻¹^4
 116
 117/-- Curvature at identity. -/
 118lemma curvature_at_identity : possibility_curvature (identity_config 0) = 2 := by
 119  simp only [possibility_curvature, identity_config, inv_one, one_pow]
 120  ring
 121
 122/-- Curvature is positive everywhere. -/
 123lemma curvature_pos (c : Config) : 0 < possibility_curvature c := by
 124  unfold possibility_curvature
 125  have h1 : 0 < c.value⁻¹ := inv_pos.mpr c.pos
 126  positivity
 127
 128/-! ## Modal Nyquist Theorem -/
 129
 130/-- **8-TICK PERIOD**: The fundamental period of modal evolution. -/
 131def modal_period : ℕ := 8
 132
 133/-- **MODAL NYQUIST LIMIT**: The finest modal resolution is one tick.
 134
 135    Possibilities that differ by less than one tick are "modally equivalent."
 136    This is analogous to the Nyquist sampling theorem:
 137    - Maximum modal frequency = 1/(2τ₀)
 138    - Modal bandwidth = 4 ticks per octave -/
 139def modal_nyquist_limit : ℕ := modal_period / 2
 140
 141/-- Two configs are **modally equivalent** if they differ by less than one tick. -/
 142def modally_equivalent (c1 c2 : Config) : Prop :=
 143  c1.value = c2.value ∧ (c1.time : ℤ) - (c2.time : ℤ) < 1 ∧ (c2.time : ℤ) - (c1.time : ℤ) < 1
 144
 145/-- Modal equivalence is reflexive. -/
 146lemma modally_equivalent_refl (c : Config) : modally_equivalent c c := by
 147  simp [modally_equivalent]
 148