prob_normalized
plain-language theorem explainer
Probabilities derived from J-cost in a finite system of energy levels sum to one for any positive inverse temperature. Statistical mechanicians working from Recognition Science cost functionals would cite this to normalize distributions before computing thermodynamic averages. The proof unfolds the probability definition, substitutes the sum of Boltzmann factors for the partition function via an auxiliary equivalence lemma, and cancels the nonzero denominator.
Claim. Let $S$ be a system with energy levels $E_i$. For inverse temperature $beta > 0$, the probabilities $P_i = exp(-beta E_i)/Z$ with partition function $Z = sum_j exp(-beta E_j)$ satisfy $sum_i P_i = 1$.
background
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. A System is a nonempty list of EnergyLevel objects. Probability for each level is the Boltzmann factor divided by the partition function Z, which sums the factors over all levels. Upstream lemmas establish that boltzmannFactor is exp(-E) in the dimensionless setting and that Z is strictly positive for beta > 0.
proof idea
Unfold probability to expose division by the partition function. Rewrite the sum as (sum of Boltzmann factors) times the reciprocal of Z. Apply partition_positive to obtain Z nonzero. Establish that the sum of Boltzmann factors equals Z by unfolding the partition definition and invoking the finset-to-list sum equivalence. Cancel via mul_inv_cancel.
why it matters
This normalization result completes the core derivation of the Boltzmann distribution from J-cost in the THERMO-001 module. It guarantees a valid probability measure before entropy or free-energy calculations in the Recognition framework. The result supports the statistical-mechanics paper proposition without invoking the phi-ladder or T8 dimension forcing directly; no downstream uses are recorded, leaving open its insertion into larger thermodynamic identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.