J_change
J_change defines the total recognition cost for evolving from configuration x to y over one octave as the sum of direct transition cost and target stasis cost. Modal logic and possibility-space analyses in Recognition Science cite it when comparing change versus stasis preferences. The definition is a direct one-line sum of the two component costs already established in the module.
claimFor positive reals $x,y>0$, the change cost is defined by $J_ {change}(x,y) := J_{transition}(x,y) + J_{stasis}(y)$, where $J_{transition}(x,y) = |ln(y/x)| · (J(x)+J(y))/2$ and $J_{stasis}(y) = 8 J(y)$.
background
The Modal.Possibility module treats configurations as positive reals equipped with a J-cost induced by the multiplicative recognizer. J_transition(x,y) is the action for a direct transition, given by the absolute log-ratio of the states times the average J-cost along the path. J_stasis(x) = 8 J(x) encodes the continuous recognition cost of maintaining a state across one eight-tick octave. Both component definitions rest on the cost functions supplied by ObserverForcing and MultiplicativeRecognizerL4, which equate recognition-event cost with J-cost.
proof idea
One-line wrapper that adds the value of J_transition x y hx hy to the value of J_stasis y.
why it matters in Recognition Science
J_change supplies the concrete dynamics criterion used by identity_prefers_stasis, prefers_change, and the rs_modal_logic_status report. It operationalizes the eight-tick octave (T7) by combining transition and maintenance costs over one period, thereby supporting the rule that the universe selects change precisely when J_change < J_stasis. The definition closes the local grammar of possibility and feeds the larger claim that identity is the unique stable state.
scope and limits
- Does not decide whether J_change(x,y) is smaller than J_stasis(x).
- Does not apply to non-positive real arguments.
- Does not encode multi-step paths inside a possibility space.
- Does not produce numerical evaluations for concrete x and y.
formal statement (Lean)
176noncomputable def J_change (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : ℝ :=
proof body
Definition body.
177 J_transition x y hx hy + J_stasis y
178
179/-- No change means only stasis cost. -/