jcost_boltzmann_monotone
plain-language theorem explainer
If the J-cost of configuration x is strictly less than that of y, then at any positive temperature the associated Boltzmann weight for x exceeds that for y. Thermal modelers in Recognition Science cite the result to confirm that equilibrium distributions select minimal-J-cost states. The short tactic proof unfolds the exponential definition, reduces the claim to an exponent comparison, and closes the inequality with division by positive T followed by linarith.
Claim. Let $x,y,T>0$. If $J(x)<J(y)$, then $e^{-J(x)/T}>e^{-J(y)/T}$, where $J$ is the J-cost functional $J(z)=(z+z^{-1})/2-1$.
background
The module JCostThermoBridge derives thermodynamic distributions from the Recognition Science J-cost functional. J-cost is the unique cost satisfying the Recognition Composition Law and is given explicitly by $J(x)=(x+x^{-1})/2-1$ (equivalently cosh(log x)-1) on positive ratios; this definition is supplied by the structure PhiForcingDerived.of. Temperature T enters as the Lagrange multiplier that enforces the average J-cost constraint, exactly as described in the module doc-comment. Upstream lemmas include LedgerFactorization.of (calibration of J on the positive reals) and SpectralEmergence.of (emergence of gauge and spin content that later selects Fermi/Bose cases).
proof idea
The proof is a direct tactic sequence. It unfolds the definition of jcostBoltzmann, invokes Real.exp_lt_exp_of_lt to reduce the claim to an inequality between the negative exponents, establishes -Jcost y/T < -Jcost x/T by applying div_lt_div_of_pos_right to the given cost inequality (using T>0), and finishes with linarith.
why it matters
The monotonicity supplies the selection principle underlying the module's main claims that Boltzmann weights minimize expected J-cost and that energy is proportional to J-cost. It sits inside the T5 J-uniqueness step of the forcing chain and supplies the classical limit before the EightTick phase constraints produce Fermi-Dirac and Bose-Einstein distributions. No downstream uses are recorded yet; the result therefore closes the classical thermodynamic bridge without yet addressing quantum statistics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.