levelCost
levelCost assigns the J-cost to an energy level by normalizing its energy against a positive reference and applying the J function, or zero if the energy is non-positive. Researchers deriving statistical mechanics from Recognition Science J-cost primitives would cite it when building expected-cost expressions for Boltzmann factors. The definition is a direct conditional that delegates to the Jcost operation on the scaled ratio.
claimFor an energy level with value $E$ and reference energy $E_0 > 0$, the level cost equals $J(E/E_0)$ if $E > 0$ and equals 0 otherwise.
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 selected under a fixed ledger-balance constraint. An EnergyLevel pairs an energy value in natural units with a positive degeneracy counting microstates. The J-cost here is the normalized form J(E/E_0) that measures cost relative to a ground-state reference, consistent with the module's core insight that cost-optimal allocation under a total-J constraint recovers the exponential form via a Lagrange multiplier.
proof idea
The definition is a direct conditional: it tests whether the level energy exceeds zero and, if so, applies Jcost to the ratio of level energy over the reference energy; otherwise it returns zero. No auxiliary lemmas are required beyond the primitive Jcost operation.
why it matters in Recognition Science
This definition supplies the per-level cost term to the downstream recognitionCost function, which computes the expected J-cost over the probability distribution and thereby connects J-cost selection to the partition function. It fills the energy-dependent step in the module's derivation of P_i = exp(-β E_i)/Z, anchoring the T5 J-uniqueness landmark to thermodynamic observables. The construction remains open on the explicit emergence of temperature as a derivative of J-cost with respect to entropy.
scope and limits
- Does not incorporate degeneracy into the returned cost value.
- Does not compute the partition function or normalized probabilities.
- Does not accept non-positive reference energies.
Lean usage
recognitionCost sys beta refEnergy hr := Finset.univ.sum (fun i => probability sys beta i * levelCost (sys.levels.get i) refEnergy hr)formal statement (Lean)
172noncomputable def levelCost (level : EnergyLevel) (refEnergy : ℝ) (hr : refEnergy > 0) : ℝ :=
proof body
Definition body.
173 if level.energy > 0 then Jcost (level.energy / refEnergy)
174 else 0
175
176/-- **THEOREM (Cost-Weighted Selection)**: The partition function Z is at least 1
177 when the system includes a zero-energy ground state. This means the Boltzmann
178 distribution is normalizable and the free energy is well-defined. -/