J_stasis_at_one
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove J_stasis(x) > 0 for any x ≠ 1.
- Does not apply to non-positive real arguments.
- Does not derive the full uniqueness statement for stable states.
- Does not address transition costs between distinct configurations.
Lean usage
have hJ1 : J_stasis 1 = 0 := J_stasis_at_oneformal statement (Lean)
160lemma J_stasis_at_one : J_stasis 1 = 0 := by unfold J_stasis; simp [J_at_one]
proof body
Term-mode proof.
161
162/-- Stasis cost is non-negative for positive configurations. -/