transiency_instability
plain-language theorem explainer
The theorem shows that the J-cost function is strictly positive for any positive real perturbation ε away from the equilibrium value 1. Researchers formalizing William James' marks of religious experience within Recognition Science would cite it to establish the instability of the zero-cost state. The proof is a direct application of the general positivity lemma for J-cost away from unity, discharging the two hypotheses via linear arithmetic.
Claim. For every real number $ε > 0$, the J-cost of $1 + ε$ is strictly positive: $J(1 + ε) > 0$.
background
In the module deriving religious experience from J-cost, William James' four marks are formalized using the J-cost function. Noetic quality corresponds to equilibrium at J-cost zero; transiency is the instability of that equilibrium, since any perturbation raises cost. The upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 for x > 0 and x ≠ 1, with the explicit form obtained by rewriting Jcost as a square divided by x and applying positivity of squares.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one. It uses linarith to confirm 0 < 1 + ε and 1 + ε ≠ 1, then invokes the lemma to obtain the strict inequality for Jcost.
why it matters
This theorem supplies the transiency field inside the ReligiousExperienceCert definition that bundles the four marks. It realizes the module claim that transiency equals instability of J = 0. In the Recognition framework it connects J-cost positivity (from the J-uniqueness step) to the philosophical reading of transient states without adding axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.