pith. machine review for the scientific record. sign in
lemma proved term proof high

J_change_self

show as:
view Lean formalization →

The identity shows that the cost of evolving a configuration to itself equals its stasis cost exactly, since the transition penalty vanishes. Researchers analyzing fixed-point stability or the dynamics criterion in Recognition Science cite this when determining when change is preferred over stasis. The term-mode proof unfolds the change-cost definition, applies the self-transition identity, and simplifies via ring.

claimFor any real number $x > 0$, the change cost from $x$ to $x$ equals the stasis cost of $x$.

background

J_stasis(x) is defined as eight times the recognition cost J(x), reflecting the eight-tick octave cycle over which a configuration must be maintained. J_change(x,y) is the sum of the transition cost from x to y plus the stasis cost at y, so that the total cost of moving and then holding the new state is captured in one expression. The module develops the dynamics criterion: a configuration evolves when the change cost to some other state is strictly lower than its own stasis cost.

proof idea

The proof is a one-line wrapper. It unfolds the definition of J_change to expose the transition term, rewrites that term to zero using the self-transition lemma, and concludes by ring normalization.

why it matters in Recognition Science

This lemma anchors the dynamics criterion by confirming that unchanged evolution reduces exactly to stasis cost, supporting the statement that only the identity fixed point is stable. It connects directly to the eight-tick octave via the factor of eight in J_stasis and to J-uniqueness in the forcing chain. As a foundational identity in the modal possibility section, it prepares threshold analyses without adding hypotheses.

scope and limits

formal statement (Lean)

 180lemma J_change_self {x : ℝ} (hx : 0 < x) : J_change x x hx hx = J_stasis x := by

proof body

Term-mode proof.

 181  unfold J_change
 182  rw [J_transition_self hx]
 183  ring
 184
 185/-! ## The Dynamics Criterion: Why Change Happens -/
 186
 187/-- **DYNAMICS CRITERION**: A configuration x evolves to y when change is cheaper than stasis.
 188
 189    This is the fundamental answer to "why does anything happen?"
 190
 191    Change occurs iff J_change(x,y) < J_stasis(x) for some y ≠ x.
 192
 193    Stasis is preferred iff x = 1 (identity is the only stable fixed point). -/

depends on (14)

Lean names referenced from this declaration's body.