prefers_change
plain-language theorem explainer
prefers_change defines a positive real x to prefer change precisely when some distinct y exists with transition-plus-maintenance cost strictly below the stasis cost at x. Modal dynamics modelers cite it as the primitive criterion answering why configurations evolve rather than remain fixed. The definition is a direct existential predicate comparing J_change and J_stasis with no auxiliary lemmas.
Claim. A positive real number $x$ prefers change when there exists $y>0$, $y≠x$, such that the sum of transition cost from $x$ to $y$ plus stasis cost at $y$ is strictly less than the stasis cost at $x$.
background
In the Modal.Possibility module the J function encodes recognition cost per the Recognition Composition Law. J_stasis(x) equals 8·J(x), the total cost over one eight-tick octave to keep configuration x unchanged. J_change(x,y) equals J_transition(x,y) plus J_stasis(y), adding the one-octave transition cost to the subsequent maintenance cost at y.
proof idea
The definition is a direct existential quantification over y and its positivity witness hy. It asserts y≠x together with the strict inequality J_transition(x,y)+J_stasis(y)<J_stasis(x). No lemmas or tactics are invoked; the body is the primitive predicate.
why it matters
This supplies the core dynamics criterion inside the modal layer, implementing the statement that change occurs exactly when cheaper than stasis. It rests on the eight-tick octave (T7) and the J-cost structure from the forcing chain, providing the formal answer to why anything happens. No immediate downstream uses are recorded, leaving its role in larger modal necessity arguments open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.