J_stasis
plain-language theorem explainer
Stasis cost accumulates the per-tick recognition expense of an unchanged configuration across one full eight-tick octave. Modal analysts cite J_stasis when comparing the zero-cost stability of the identity state against any transition that incurs positive J_change. The definition is a direct scaling of the base J function by the octave length.
Claim. The stasis cost is defined by $J_mathrm{stasis}(x) := 8 J(x)$, where the base cost is $J(x) = frac12(x + x^{-1}) - 1$ for $x > 0$.
background
In the Modal.Possibility module, a configuration is labeled by a positive real $x$ whose distance from 1 measures departure from the identity event. The sibling definition J supplies the fundamental per-tick cost $J(x) = frac12(x + x^{-1}) - 1$, the unique function satisfying d'Alembert's relation plus normalization at the identity. The module develops modal possibility spaces whose paths interleave transitions and stasis intervals; the eight-tick period follows from the T7 octave forced by the self-similar fixed point phi.
proof idea
One-line definition that multiplies the base J cost by eight to cover the full octave.
why it matters
J_stasis supplies the maintenance term inside J_change and the zero-cost anchor used by identity_prefers_stasis to prove that only the identity configuration is stable. It accounts for the continuous recognition cost required by the eight-tick cycle (T7) and the Recognition Composition Law. The definition is invoked by rs_modal_logic_status and by the lemmas establishing that identity lies in every possibility space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.