J_transition

formal source

 123    - J_transition(x,x) = 0 (no change = no cost)
 124    - J_transition(x,y) = J_transition(y,x) (symmetric)
 125    - J_transition(x,1) = |ln x| · J(x) / 2 (approaching identity is cheap for x ≈ 1) -/
 126noncomputable def J_transition (x y : ℝ) (_ : 0 < x) (_ : 0 < y) : ℝ :=
 127  |Real.log (y / x)| * ((J x + J y) / 2)
 128
 129/-- Transition to self has zero cost. -/
 130lemma J_transition_self {x : ℝ} (hx : 0 < x) : J_transition x x hx hx = 0 := by
 131  unfold J_transition
 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) -/