J_stasis_at_one
plain-language theorem explainer
The lemma shows that the cost of maintaining the identity configuration over one full octave is zero. Modal theorists in Recognition Science cite it when proving that only the identity is stable under stasis preference. The proof proceeds by a direct unfolding of the stasis definition followed by simplification with the unit cost lemma.
Claim. The cost of stasis at the multiplicative identity is zero: $J_ {stasis}(1) = 0$, where $J_{stasis}(x) := 8 J(x)$ and $J$ is the recognition cost function.
background
In the Modal.Possibility module, configurations are positive reals equipped with the recognition cost function J. The stasis cost is defined as eight times the base cost, J_stasis(x) = 8 J(x), to account for the continuous recognition payment required to keep a configuration unchanged across one octave cycle. This rests on the normalization J(1) = 0 from the CostAlgebra module, which encodes the algebraic fact that the multiplicative identity carries zero cost.
proof idea
The proof is a one-line wrapper that unfolds the definition of J_stasis and applies the lemma J_at_one to obtain the result at argument 1.
why it matters
This lemma is invoked directly by identity_prefers_stasis, which concludes that the identity is the unique configuration preferring stasis. It supplies the zero-cost anchor for the modal stability argument and aligns with the eight-tick octave structure in the forcing chain. No open scaffolding questions are addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.