EnergyLevel
plain-language theorem explainer
EnergyLevel packages a real energy value, a positive natural-number degeneracy, and the positivity witness into a single record. Researchers deriving the Boltzmann distribution from J-cost in Recognition Science cite this structure when assembling collections of states for cost-weighted selection. The declaration is a bare structure definition whose only content is the three field declarations.
Claim. An energy level is a record $(E, g, p)$ where $E$ is a real number, $g$ is a positive natural number, and $p$ is a witness that $g > 0$.
background
The module THERMO-001 derives the Boltzmann distribution from Recognition Science's J-cost functional. Each state carries a recognition cost J(x); lower-cost states are more probable, and the cost-optimal allocation under a fixed ledger balance recovers the exponential form. Energy is imported as the alias ℝ from RSNativeUnits. Upstream structures such as LedgerFactorization.of supply the calibration of J, while PhiForcingDerived.of encodes the J-cost itself. IntegrationGap.A and related constants fix the active-edge count and φ-power balance at D = 3.
proof idea
This is a structure definition with no proof body. The three fields are declared directly: energy of type ℝ, degeneracy of type ℕ, and deg_pos of type degeneracy > 0. No lemmas or tactics are invoked.
why it matters
EnergyLevel supplies the atomic data type for the cost-weighted state selection that yields the Boltzmann factor. It is instantiated inside the System structure and consumed by boltzmannFactor, levelCost, and the normalization lemmas that follow. The declaration therefore fills the first concrete step of the paper proposition on statistical mechanics from Recognition Science, linking the J-cost primitive to the partition function Z = Σ g_i exp(-β E_i).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.