levelCost
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.