jcost_boltzmann_pos
plain-language theorem explainer
J-cost Boltzmann weights remain strictly positive for every positive energy ratio x and temperature T. Thermodynamic derivations in the Recognition Science framework cite this to guarantee that partition functions and state probabilities stay positive. The proof is a one-line wrapper invoking the positivity of the real exponential function on the weight definition.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$. For all real $x > 0$ and $T > 0$, the J-cost Boltzmann weight satisfies $e^{-J(x)/T} > 0$.
background
The J-Cost to Thermodynamics Bridge module connects the Recognition Science J-cost functional to Boltzmann, Fermi-Dirac, and Bose-Einstein distributions. J-cost is the derived cost of a multiplicative recognizer comparator, given explicitly by $J(x) = (x + x^{-1})/2 - 1$ on positive ratios; temperature T serves as the Lagrange multiplier that enforces the average J-cost constraint in the equilibrium distribution.
proof idea
This is a one-line wrapper that applies Real.exp_pos to the definition of jcostBoltzmann.
why it matters
The result feeds the partition_pos theorem in the same module, which establishes positivity of the full partition function. It fills the step that converts J-cost minimization into positive Boltzmann factors, consistent with the eight-tick octave and the J-uniqueness fixed point in the forcing chain. No open scaffolding questions are resolved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.