off_equilibrium_cost
plain-language theorem explainer
Off-equilibrium states incur a strictly positive J-cost in the Recognition Science derivation of statistical mechanics. Derivations of the partition function and ensemble counts cite this to separate the equilibrium J = 0 contribution from all others. The argument is a direct invocation of the J-cost positivity lemma under the given positivity and inequality hypotheses.
Claim. Let $r$ be a positive real number not equal to 1. Then the J-cost of $r$ is strictly positive: $J(r) > 0$.
background
The module Statistical Mechanics from RS constructs macroscopic thermodynamics from the J-cost function of Recognition Science. The partition function takes the form $Z = sum exp(-J(state)/kT)$, reducing to $Z = 1$ when only the equilibrium state with $J = 0$ is present. Upstream, the lemma Jcost_pos_of_ne_one establishes that $J(x) > 0$ whenever $x > 0$ and $x neq 1$, via rewriting as a square over a positive denominator.
proof idea
The proof consists of a single application of the lemma Jcost_pos_of_ne_one, passing the hypotheses 0 < r and r ≠ 1 directly to it.
why it matters
This result populates the off_equil_positive component of the StatMechCert definition, which bundles the ensemble count, equilibrium partition, and off-equilibrium positivity into a single certificate. It supports the framework claim that equilibrium dominates the partition function while non-equilibrium states add positive cost, consistent with the RS forcing chain and the J-uniqueness property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.