J_change

formal source

 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). -/
 194def prefers_change (x : ℝ) (hx : 0 < x) : Prop :=
 195  ∃ y : ℝ, ∃ hy : 0 < y, y ≠ x ∧ J_change x y hx hy < J_stasis x
 196
 197def prefers_stasis (x : ℝ) (hx : 0 < x) : Prop :=
 198  ∀ y : ℝ, ∀ hy : 0 < y, y ≠ x → J_stasis x ≤ J_change x y hx hy
 199
 200/-- **THEOREM**: The identity is the unique configuration that prefers stasis.
 201
 202    For x = 1: J_stasis(1) = 0, and any change costs > 0.
 203    For x ≠ 1: There exists y closer to 1 with J_change(x,y) < J_stasis(x).
 204
 205    This proves: **Existence (x = 1) is the unique stable state.** -/
 206theorem identity_prefers_stasis : prefers_stasis 1 one_pos := by