gibbs_log_form
plain-language theorem explainer
The log-probability under the Gibbs measure on a recognition system equals minus the J-cost of the evaluated state divided by the system's recognition temperature minus the log of the partition function. Thermodynamic derivations that obtain the exponential distribution from constrained optimization on many-body ledgers cite this identity to show the form is forced rather than postulated. The proof is a direct term reduction that unfolds the measure and weight definitions, invokes positivity of the partition function, and rewrites via the log-1
Claim. Let $p$ be the Gibbs measure on a recognition system with recognition temperature $T_R$, let $J$ denote the J-cost functional, let $X$ map states to real values, and let $Z$ be the partition function. Then for any state $ω$, $log p(ω) = -J(X(ω))/T_R - log Z$.
background
The JCostEntropyAncestor module derives the Gibbs form as a theorem of constrained optimization rather than a definition. J-cost is the functional $J(x) = (x + x^{-1})/2 - 1$ that satisfies the Recognition Composition Law; its shifted version $H(x) = J(x) + 1 = (x + x^{-1})/2$ converts the law into the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. The module works in the setting of many-body ledgers where the number of microstates realizing a macrodistribution $p$ is the multinomial coefficient, which by Stirling yields Shannon entropy $H(p) = -∑ p_i log p_i$ as the leading term in the log-count. The average J-cost is held fixed, and the most probable $p$ is obtained by Lagrange multipliers, producing the exponential weights with $T_R$ emerging as the multiplier.
proof idea
The proof is a one-line term reduction. It unfolds gibbs_measure and gibbs_weight, obtains positivity of the partition function from the upstream lemma partition_function_pos, and rewrites the resulting expression with log_div (applied to the exponential numerator and positive denominator) followed by log_exp.
why it matters
This supplies the gibbs_log field of the EntropyAncestorCertificate, which also records the domination inequality J-cost ≥ (log x)^2 / 2 and the non-negativity of J-cost divergence. The result therefore closes the backward direction of the module: it shows why the Gibbs weights are forced by stationarity on the ledger rather than chosen, thereby making Shannon entropy a quadratic shadow of J-cost. In the Recognition framework it links the CostAlgebra reparametrization H directly to the thermodynamic structures of RecognitionThermodynamics and MaxEntFromCost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.