gibbs_form_is_unique
plain-language theorem explainer
Any distribution q on states that takes the explicit exponential form exp(−J(X(ω))/TR) normalized by its partition function coincides exactly with the Gibbs measure of the recognition system. Workers deriving maximum-entropy states from constrained J-cost functionals cite this uniqueness to confirm the stationary distribution is forced rather than assumed. The proof is a one-line term rewrite that substitutes the hypothesis directly into the target definition.
Claim. Let $q$ be any function on the state space such that $q(ω) = exp(−J(X(ω))/T_R) / ∑_{ω′} exp(−J(X(ω′))/T_R)$ for every state $ω$, where $T_R$ is the recognition temperature of the system. Then $q$ equals the Gibbs measure associated to the system and the cost function $X$ at every state.
background
The module shows that J-cost functions as the ancestor of Shannon entropy: for many independent recognition subsystems the most probable macrodistribution under fixed average J-cost maximizes the multinomial count, which by Stirling reduces to maximizing Shannon entropy H(p) = −∑ p_i log p_i. J-cost is the functional J(x) = ½(x + x⁻¹) − 1 that obeys the Recognition Composition Law; its shifted form H(x) = J(x) + 1 satisfies the d’Alembert equation used in the ledger factorization. The Gibbs measure is the normalized exponential weight exp(−J(X(ω))/T_R)/Z that arises as the unique critical point of the Lagrangian H(q) − β⟨J⟩_q − λ(Σq − 1).
proof idea
The proof is a term-mode one-liner: introduce the state ω, rewrite the goal by the hypothesis that q matches the exponential form, and close by reflexivity.
why it matters
The result supplies the uniqueness half of the thermodynamic bridge: the Gibbs form is not postulated but forced by stationarity of the constrained entropy functional on many-body ledgers. It completes the ancestor hierarchy in which J-cost dominates squared-log information content and Shannon entropy appears only as the quadratic shadow. The theorem sits inside the forcing chain at the T5 J-uniqueness step and supports the claim that T_R is derived rather than free. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.