J_pos_of_ne_one
plain-language theorem explainer
The cost function J is strictly positive for every positive real not equal to one. Modal arguments in Recognition Science cite this to establish that any non-identity configuration carries positive cost and therefore tends to actualize. The short proof obtains non-negativity of J from an upstream lemma, then rules out the zero case by the characterization that J vanishes only at one.
Claim. Let $J(x) := {1/2}(x + x^{-1}) - 1$. For every real $x > 0$ with $x ≠ 1$, one has $J(x) > 0$.
background
The function J is the fundamental cost in Recognition Science, defined by $J(x) = {1/2}(x + x^{-1}) - 1$. It is the unique cost satisfying d'Alembert's principle together with normalization and calibration (T5). In the Modal.Possibility module, configurations are positive reals carrying this cost, with the identity configuration at $x=1$ where J attains its global minimum of zero. Upstream results in the same module establish non-negativity of J for positive arguments and the precise location of its zero set.
proof idea
The proof first applies the non-negativity lemma for J. It then performs a case split on whether the value is strictly positive or zero. The strict case is immediate. The zero case is discharged by the characterization that J vanishes only at one, contradicting the hypothesis $x ≠ 1$.
why it matters
This lemma is invoked directly by actualize_decreases_cost, which shows that actualization lowers cost, and by why_anything_happens, the master modal theorem that answers why change occurs by comparing the positive stasis cost $8·J(x)$ against the cheaper transition to identity. It supplies the positivity consequence of the J-uniqueness result (T5) inside the forcing chain and is required for any modal argument that treats non-identity states as unstable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.