off_equilibrium_cost
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the explicit algebraic form of the J-cost function.
- Does not quantify the magnitude of the cost for particular states.
- Does not incorporate the effects of temperature on the distribution.
- Does not extend to continuous state spaces or field theories.
Lean usage
theorem use_off_equilibrium (r : ℝ) (hr : 0 < r) (hne : r ≠ 1) : 0 < Jcost r := off_equilibrium_cost hr hneformal statement (Lean)
33theorem off_equilibrium_cost {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
34 0 < Jcost r := Jcost_pos_of_ne_one r hr hne
proof body
35