J_transition_symm

formal source

 132  simp [div_self (ne_of_gt hx)]
 133
 134/-- Transition cost is symmetric. -/
 135lemma J_transition_symm {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
 136    J_transition x y hx hy = J_transition y x hy hx := by
 137  unfold J_transition
 138  congr 1
 139  · -- Show |log(y/x)| = |log(x/y)|
 140    have h1 : Real.log (y / x) = -Real.log (x / y) := by
 141      rw [Real.log_div (ne_of_gt hy) (ne_of_gt hx)]
 142      rw [Real.log_div (ne_of_gt hx) (ne_of_gt hy)]
 143      ring
 144    rw [h1, abs_neg]
 145  · ring
 146
 147/-! ## Cost of Stasis vs Cost of Change -/
 148
 149/-- **COST OF STASIS**: The cost for a configuration to remain unchanged.
 150
 151    In RS, even "staying the same" has a recognition cost because:
 152    1. The universe is constantly recognizing itself (8-tick cycle)
 153    2. Maintaining identity requires continuous cost payment
 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)