recognitionCost
plain-language theorem explainer
The recognitionCost definition computes the expected J-cost of energy ratios for a system's levels under a probability distribution at inverse temperature beta, defaulting to zero unless the reference energy is positive. Researchers deriving statistical mechanics from recognition principles would cite it when expressing thermodynamic expectations in terms of the J-functional. The definition implements this via a conditional finite sum that weights each level's cost by its probability only for positive reference energy.
Claim. For a system $S$ with energy levels, inverse temperature $β$, and reference energy $E_r > 0$, the recognition cost equals $∑_i p_i · J(E_i / E_r)$, where $p_i$ is the probability of level $i$ and $J$ is the cost of the energy ratio.
background
The module THERMO-001 derives the Boltzmann distribution from Recognition Science's J-cost functional, where states with lower J-cost are more probable and the cost-optimal allocation under a fixed total cost constraint yields $P_i = exp(-β E_i)/Z$. A System is a nonempty list of EnergyLevel structures. The J-cost itself is supplied by upstream definitions: cost from MultiplicativeRecognizerL4 as the derivedCost of a comparator on positive ratios, and cost from ObserverForcing as Jcost of a recognition event state. Probability is taken from QuantumLedger as the Born-rule norm squared of amplitudes.
proof idea
The definition is a direct conditional expression: when refEnergy > 0 it returns the Finset.univ sum of probability sys beta i multiplied by levelCost of the i-th level (using the supplied hr witness), otherwise zero. It applies the probability and cost functions from the listed upstream declarations without further reduction.
why it matters
This definition supplies the recognition cost that the downstream recognition_cost_well_defined theorem simply verifies is well-defined for positive reference energy. It realizes the module's core step of expressing thermodynamic expectations via expected J-cost, linking directly to the J-uniqueness (T5) and phi-ladder structure of the forcing chain. The construction closes one link in the derivation of Boltzmann statistics from the Recognition Composition Law without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.