possibility_curvature

formal source

 111
 112    At identity (c = 1): κ(1) = 2
 113    This curvature determines how "spread out" possibilities are. -/
 114noncomputable def possibility_curvature (c : Config) : ℝ :=
 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