energyFromJCost
plain-language theorem explainer
The definition sets energy equal to a positive reference scale E₀ multiplied by the J-cost of configuration ratio x. Researchers deriving Boltzmann weights or free-energy minima from Recognition Science would cite it to anchor thermodynamic quantities in the J-cost functional. It is realized as a direct scaling that passes non-negativity and the x=1 minimum through from the underlying J-cost.
Claim. Energy of a configuration with ratio $x$ is $E = E_0 J(x)$ where $J(x) = (x + x^{-1})/2 - 1$ and $E_0 > 0$.
background
The J-Cost to Thermodynamics Bridge module links the J-cost functional to thermodynamic distributions. J-cost is defined as $J(x) = (x + x^{-1})/2 - 1$ for positive ratios x; upstream, the cost of a recognition event is its J-cost (ObserverForcing.cost) and the cost induced by a multiplicative recognizer is the derived cost of its comparator (MultiplicativeRecognizerL4.cost). The module doc-comment states that the Boltzmann factor emerges as the distribution minimizing average J-cost subject to constraints, with temperature acting as the Lagrange multiplier for the J-cost constraint.
proof idea
The definition is a one-line wrapper that multiplies the reference energy E₀ by Jcost x, inheriting non-negativity and the minimum at unity directly from the J-cost lemmas.
why it matters
This supplies the energy-Jcost proportionality used by the parent theorem jcost_thermo_fundamentals, which assembles the full connection to Boltzmann, Fermi-Dirac and Bose-Einstein distributions. It realizes the first main theorem listed in the module doc-comment and anchors the mapping from J-cost to energy that underpins the eight-tick octave and phase constraints in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.