probability
plain-language theorem explainer
Assigns to energy level i the normalized weight given by its Boltzmann factor at inverse temperature beta divided by the system partition function. Researchers deriving statistical mechanics from recognition cost cite this when computing state occupation numbers under fixed J-cost. The definition is a direct ratio after indexing into the list of levels.
Claim. $P_i = e^{-β E_i}/Z$ where $E_i$ is the energy of level i, β is inverse temperature, and Z is the sum of Boltzmann factors over all levels in the system.
background
A System is a structure holding a nonempty list of EnergyLevel entries. The module derives the Boltzmann distribution from Recognition Science J-cost, where states are selected by minimizing total recognition cost subject to a ledger constraint; the Lagrange multiplier for that constraint supplies β. Upstream boltzmannFactor definitions supply the unnormalized weight exp(-Ea/kT) or exp(-barrier), while the partition function normalizes the distribution.
proof idea
One-line definition that indexes the level list, applies boltzmannFactor to the selected level and beta, then divides by partitionFunction.
why it matters
Supplies the occupation probability referenced by audit summaries, coincidence bounds, and resolution-time structures in the CPM and Complexity modules. It realizes the explicit key result P_i = exp(-β E_i)/Z stated in the module doc-comment for THERMO-001. The definition therefore anchors the cost-weighted derivation of statistical mechanics inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.