gibbs_measure_sum_one
plain-language theorem explainer
Gibbs measure normalization to unity holds for any finite nonempty state space equipped with a recognition system of positive temperature. Researchers extending Recognition Science to finite-temperature statistical mechanics cite this when constructing equilibrium distributions from J-cost functions. The proof is a direct algebraic reduction that unfolds the measure and partition definitions then invokes positivity of the partition function.
Claim. Let $T_R > 0$ be the recognition temperature of a system and let $X : Ω → ℝ$ be a state function on a finite nonempty set $Ω$. The associated Gibbs measure $μ(ω) = w(ω) / Z$, where $w(ω)$ is the un-normalized Gibbs weight and $Z = ∑_ω w(ω)$ is the partition function, satisfies $∑_{ω ∈ Ω} μ(ω) = 1$.
background
The RecognitionThermodynamics module extends zero-temperature J-minimization to finite recognition temperature $T_R$. A RecognitionSystem is the structure carrying a positive real $T_R$ (with derived beta = 1/$T_R$). The Gibbs measure is the normalized distribution $μ(ω) = $ gibbs_weight(sys, X(ω)) / Z, where the partition function Z sums the weights exp(−J(X(ω))/$T_R$) over the finite set Ω. The module documentation states that this construction recovers the Born-rule weight from the underlying cost function J(x) = ½(x + 1/x) − 1.
proof idea
The term proof unfolds gibbs_measure and partition_function, rewrites the sum as a single division by the partition function, and applies div_self to the already-established positivity of the partition function.
why it matters
The result supplies the sum-one axiom required to view the Gibbs measure as a ProbabilityDistribution. It is invoked directly by gibbsPD (which packages the equilibrium reference) and thereby by secondLawCert and the free-energy minimization theorems in MaxEntFromCost. The declaration therefore closes the normalization step that lets the finite-temperature extension of Recognition Science inherit the J-descent dynamics of the zero-temperature foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.