identity_prefers_stasis
plain-language theorem explainer
The configuration with value 1 is the unique point at which stasis cost vanishes while every transition to a different positive value incurs nonnegative cost. Modal extensions of Recognition Science cite this result to anchor the possibility operator at the fixed point of the dynamics. The proof is a direct nonnegativity argument that unfolds the cost definitions and applies the normalization J(1)=0 together with nonnegativity of J and its derived quantities.
Claim. The configuration $x=1$ satisfies prefers_stasis: $J_ {stasis}(1)=0$ and $J_{change}(1,y)≥0$ for every $y>0$.
background
In the Modal.Possibility module the possibility operator collects configurations reachable at finite cost with non-increasing J-cost. The auxiliary definitions are J_stasis(x) := 8 J(x), the recognition cost of holding x unchanged over one octave, and J_change(x,y) := J_transition(x,y) + J_stasis(y), the total cost of moving from x to y and then maintaining y. Upstream, J_at_one supplies the normalization J(1)=0, the algebraic statement that the multiplicative identity carries zero recognition cost.
proof idea
The tactic proof introduces an arbitrary y>0, replaces J_stasis(1) by 0 via J_stasis_at_one, unfolds J_change, and splits the sum with add_nonneg. Each summand is shown nonnegative by J_at_one.ge, J_nonneg, J_stasis_nonneg, and the elementary facts that absolute value and division by a positive constant preserve nonnegativity.
why it matters
This supplies the base case for the possibility_status report in the same module and confirms that only the identity is stable under J-cost. It instantiates the doc-comment claim that existence (x=1) is the unique stable state, aligning with the self-similar fixed point at T6 of the UnifiedForcingChain. The result closes one link in the modal extension by exhibiting the sole configuration that prefers to remain unchanged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.