J_stasis_nonneg

formal source

 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.
 188
 189    This is the fundamental answer to "why does anything happen?"
 190
 191    Change occurs iff J_change(x,y) < J_stasis(x) for some y ≠ x.
 192
 193    Stasis is preferred iff x = 1 (identity is the only stable fixed point). -/