recognitionCost
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not define or compute costs when reference energy is non-positive.
- Does not enforce or prove normalization of the probability distribution.
- Does not specify the explicit form of levelCost beyond its dependence on the J-functional.
- Does not address continuous energy spectra or infinite state spaces.
formal statement (Lean)
239noncomputable def recognitionCost (sys : System) (beta : ℝ) (refEnergy : ℝ) : ℝ :=
proof body
Definition body.
240 if hr : refEnergy > 0 then
241 (Finset.univ.sum fun i =>
242 probability sys beta i * levelCost (sys.levels.get i) refEnergy hr)
243 else 0
244
245/-- **THEOREM**: The recognition cost is well-defined for positive reference energy. -/