J_stasis

formal source

 154    3. J(x) is paid per tick, not just for change
 155
 156    J_stasis(x) = 8 · J(x) (cost over one octave to maintain x) -/
 157noncomputable def J_stasis (x : ℝ) : ℝ := 8 * J x
 158
 159/-- Stasis at identity is free. -/
 160lemma J_stasis_at_one : J_stasis 1 = 0 := by unfold J_stasis; simp [J_at_one]
 161
 162/-- Stasis cost is non-negative for positive configurations. -/
 163lemma J_stasis_nonneg {x : ℝ} (hx : 0 < x) : 0 ≤ J_stasis x := by
 164  unfold J_stasis
 165  apply mul_nonneg (by norm_num : (0:ℝ) ≤ 8) (J_nonneg hx)
 166
 167/-- **COST OF CHANGE**: The cost to evolve from x to y over one octave.
 168
 169    J_change(x,y) = J_transition(x,y) + J_stasis(y)
 170
 171    This includes:
 172    1. The transition cost to get from x to y
 173    2. The stasis cost to maintain y for one octave
 174
 175    The universe chooses change when J_change < J_stasis. -/
 176noncomputable def J_change (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : ℝ :=
 177  J_transition x y hx hy + J_stasis y
 178
 179/-- No change means only stasis cost. -/
 180lemma J_change_self {x : ℝ} (hx : 0 < x) : J_change x x hx hx = J_stasis x := by
 181  unfold J_change
 182  rw [J_transition_self hx]
 183  ring
 184
 185/-! ## The Dynamics Criterion: Why Change Happens -/
 186
 187/-- **DYNAMICS CRITERION**: A configuration x evolves to y when change is cheaper than stasis.