prefers_stasis
plain-language theorem explainer
The definition states that a positive real number satisfies the inequality between its stasis cost and the change cost to any other positive real for all distinct alternatives. Researchers working on modal stability in Recognition Science would cite this definition when establishing uniqueness of the identity configuration. The definition is a direct encoding of the stasis preference condition using the combined transition and stasis cost function.
Claim. A number $x > 0$ prefers stasis if the stasis cost at $x$ is at most the change cost from $x$ to $y$ for all $y > 0$ with $y ≠ x$, where the change cost is the sum of the transition cost from $x$ to $y$ and the stasis cost at $y$.
background
In the Modal.Possibility module the family of cost functions measures recognition cost on the real line. The stasis cost is the cost of remaining at a state for one octave; the change cost adds the transition cost to the stasis cost at the target. The upstream identity definition places the zero-cost point at state value 1. The module imports LawOfExistence and works inside the Recognition framework where the cost satisfies the composition law and the fixed-point structure.
proof idea
The declaration is the direct definition of the predicate as the stated universal quantification over alternative states of the inequality between stasis and change costs; no tactics or lemmas are applied inside the body.
why it matters
The definition supplies the antecedent for the downstream theorem that concludes the identity configuration is the unique stable state. It supplies the modal layer that converts the uniqueness property into a stability statement inside the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.