J_stasis_nonneg
plain-language theorem explainer
J_stasis_nonneg establishes that the stasis cost 8 J(x) remains non-negative for every positive real x. Modal analysts in Recognition Science cite the result when showing that only the identity configuration can be stable under pure stasis preference. The proof is a direct term-mode reduction that unfolds the definition and applies the non-negativity of multiplication together with the already-proved non-negativity of J.
Claim. For every positive real number $x$, $0$ is less than or equal to $8 J(x)$, where $J$ is the base recognition cost function.
background
The Modal.Possibility module works with positive real configurations and defines J_stasis(x) explicitly as eight times the base J-cost. This eight-fold multiplier comes from the octave constant (eight ticks) that appears in both Constants and MusicalScale. The surrounding development imports LawOfExistence and relies on the cost functions already constructed in ObserverForcing and MultiplicativeRecognizerL4; those upstream definitions supply the non-negativity property of J that the present lemma invokes.
proof idea
The proof is a one-line term-mode wrapper. It unfolds J_stasis to expose the product 8 * J x, then applies mul_nonneg with the numeric fact 0 ≤ 8 (obtained by norm_num) and the upstream lemma J_nonneg applied to the hypothesis 0 < x.
why it matters
The lemma is used directly by identity_prefers_stasis, which concludes that only the identity configuration prefers stasis. It therefore supplies a key non-negativity step in the modal stability argument of the Recognition framework, tying the eight-tick octave period to the claim that existence at x = 1 incurs zero stasis cost. The result sits inside the forcing chain after the definition of J and before the uniqueness theorems that select D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.