why_anything_happens
plain-language theorem explainer
Any configuration c with value x ≠ 1 satisfies J_stasis(x) > 0. Modal theorists working in Recognition Science cite this as the master theorem grounding why change occurs rather than stasis. The term proof unfolds the eight-fold multiplier in J_stasis and applies the sibling positivity lemma J_pos_of_ne_one after a norm_num witness for the constant factor.
Claim. Let x be the value of a configuration c with x ≠ 1 and x > 0. Then the stasis cost satisfies 8 J(x) > 0, where J(x) = ½(x + x^{-1}) - 1.
background
In the Modal.Possibility module a Config is a structure holding a positive real value x, a tick coordinate, and the bound |log x| ≤ 16. The J-cost is the function J(x) = ½(x + x^{-1}) - 1 calibrated by d'Alembert factorization and phi-forcing; J_stasis(x) := 8 J(x) records the recognition cost of holding x fixed over one eight-tick octave. The module develops a grammar of possibility in which reachable states are those reachable at finite J-transition cost.
proof idea
The term proof unfolds J_stasis to expose the product 8 · J(c.value), applies mul_pos with the explicit witness (0 : ℝ) < 8 obtained by norm_num, and closes by exact application of the sibling lemma J_pos_of_ne_one using the positivity hypothesis on c and the assumption c.value ≠ 1.
why it matters
The declaration supplies the core positivity fact consumed by the status reports rs_modal_logic_status and possibility_status. It realizes the master modal theorem that stasis away from identity is costly, thereby answering why change is preferred. In the framework it directly instantiates the eight-tick octave (T7) and J-uniqueness (T5) from the unified forcing chain, closing a link from the imported LawOfExistence foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.