nonequilibrium_cost
plain-language theorem explainer
Non-equilibrium states require strictly positive J-cost in Recognition Science thermochemistry. A physicist constructing thermodynamic potentials from the J-function would cite this to confirm that work is expended away from the free-energy minimum. The proof is a one-line wrapper applying the J-cost positivity lemma to the supplied ratio r.
Claim. For every real number $r$ with $0 < r$ and $r ≠ 1$, the J-cost satisfies $0 < J(r)$, where $J$ is the cost function whose vanishing marks equilibrium.
background
The ThermochemistryFromRS module derives five canonical thermodynamic potentials (U, H, F, G, Ω) from Recognition Science, setting them equal to configDim D = 5. Equilibrium chemical states correspond to J = 0 (free-energy minimum) while non-equilibrium states require J > 0 (work to equilibrate). The J-cost function is imported from the Cost module.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one (from Cost, JcostCore, and LocalCache) to the parameters r, hr, and hne. That lemma rewrites Jcost via its squared form Jcost_eq_sq and invokes positivity of squares together with division.
why it matters
This result supplies the nonequil field of thermochemistryCert, which also records the five potentials and chemical_equilibrium. It completes the RS thermochemistry certification by confirming the sign of J away from unity, consistent with J-uniqueness (T5) and the Recognition Composition Law that govern the cost function throughout the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.