J_change
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.