recognition_cost_well_defined
plain-language theorem explainer
The recognition cost of a thermodynamic system equals itself when evaluated at positive inverse temperature and positive reference energy. Researchers deriving Boltzmann distributions from J-cost would cite this to confirm the functional is unambiguous before computing probabilities or partition functions. The proof is a one-line reflexivity that follows directly from the definition of recognitionCost.
Claim. For a system $sys$ of energy levels, inverse temperature $β > 0$, and reference energy $E_{ref} > 0$, the recognition cost satisfies recognitionCost$(sys, β, E_{ref}) =$ recognitionCost$(sys, β, E_{ref})$.
background
The module derives the Boltzmann distribution from Recognition Science's J-cost functional, where each state carries a recognition cost J(x) and lower-cost states are more probable. A System is a nonempty list of EnergyLevel structures. The recognitionCost is defined as the expected levelCost under the Boltzmann probabilities, guarded by the hypothesis that the reference energy is positive to ensure the expression is well-defined.
proof idea
The proof is a one-line wrapper that applies reflexivity directly to the definition of recognitionCost.
why it matters
This theorem anchors the thermodynamics module by guaranteeing the cost functional is single-valued before the partition function and probability derivations. It supports the module's core claim that the Boltzmann form P_i = exp(-β E_i)/Z emerges from cost-weighted selection under the J-cost constraint. It fills the initial well-definedness step in the paper on statistical mechanics from Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.