prob_nonneg
plain-language theorem explainer
Probabilities in the Boltzmann distribution derived from J-cost are non-negative. A researcher building statistical mechanics inside Recognition Science would cite this result to confirm the distribution forms a valid measure. The proof reduces the claim to non-negativity of a ratio by unfolding the definition and applying arithmetic lemmas on multiplication and division.
Claim. Let $sys$ be a collection of energy levels and let $β > 0$ be an inverse temperature. For each index $i$, the Boltzmann probability $p_i(β)$ of the $i$-th level satisfies $p_i(β) ≥ 0$.
background
The module derives the Boltzmann distribution from the J-cost functional. A System is a non-empty list of energy levels. The probability for level $i$ at inverse temperature $β$ is the normalized Boltzmann factor, obtained by dividing the cost-weighted term by the partition function. This construction re-uses the boltzmannFactor appearing in chemistry and information modules, which returns $exp(-E)$ or $exp(-Ea/kT)$ depending on context. The local setting is the derivation of statistical mechanics from Recognition Science cost constraints, where $β$ emerges as a Lagrange multiplier enforcing fixed total J-cost.
proof idea
The proof unfolds probability and boltzmannFactor to expose a ratio. It applies div_nonneg, confirms the numerator is non-negative via mul_nonneg on a cast natural number and a positive exponential, and invokes the positivity of the partition function from the upstream partition_positive lemma.
why it matters
This result supplies the non-negativity axiom required by the ProbDist structure in variational free energy derivations from the Recognition Composition Law. It also parallels the corresponding non-negativity statement in the Quantum Ledger. Within the framework it confirms that cost-weighted selection, built on T5 J-uniqueness and the phi fixed point, produces a valid probability distribution and thereby supports the emergence of thermodynamics from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.