jcostBoltzmann
plain-language theorem explainer
Recognition Science replaces energy with the J-cost functional in the Boltzmann factor. The definition supplies exp(-J(x)/T) as the probability weight for ratio x at temperature T > 0. Equilibrium derivations cite it when minimizing average J-cost under thermal constraints. It is a direct one-line transcription of the exponential form that enables downstream positivity and monotonicity results.
Claim. The J-cost Boltzmann factor for a state with ratio $x > 0$ at temperature $T > 0$ is given by $e^{-J(x)/T}$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The J-Cost to Thermodynamics Bridge module links Recognition Science's J-cost functional to thermodynamic distributions by substituting J-cost for energy in the Boltzmann factor. J(x) = ½(x + x^{-1}) - 1 quantifies the recognition cost of a ratio x, and temperature T acts as the Lagrange multiplier enforcing the J-cost constraint at equilibrium. The module states that this yields P(E) ∝ exp(-β J(E/E₀)) and connects J-cost minimization to free-energy minimization.
proof idea
This is a direct definition that applies Real.exp to the term -Jcost x / T. No lemmas are invoked; the body is a one-line wrapper around the exponential function with the J-cost term supplied by the Cost module.
why it matters
The definition is invoked by partitionFunction and stateProbability, and by the theorems jcost_boltzmann_pos, jcost_boltzmann_max_at_unity, and jcost_boltzmann_monotone. It supplies the Boltzmann weight inside the jcost_thermo_fundamentals theorem that connects J-cost to free energy and to spin-statistics via 8-tick phases. In the Recognition framework it realizes the thermal selection of low-cost states consistent with T5 J-uniqueness and T7 eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.