lagrange_forces_gibbs
plain-language theorem explainer
If a probability distribution q on finite Ω satisfies log q(ω) = −β Jcost(X(ω)) − c for β > 0 and constant c, then q equals the Gibbs measure at recognition temperature 1/β. Thermodynamic derivations in Recognition Science cite this to derive the exponential form as the forced outcome of Lagrange maximization of entropy under fixed average J-cost. The proof algebraically rewrites the stationarity equation into factored exponentials, extracts the partition function from the normalization ∑q = 1, and matches the unfolded definition of gibbs_meas.
Claim. Let $q$ be a positive probability distribution on finite set $Ω$ and $X:Ω→ℝ$ a J-cost assignment. If there exist $β>0$ and $c∈ℝ$ such that $log q(ω)=−β J(X(ω))−c$ for every $ω$, then $q(ω)$ equals the Gibbs measure $exp(−J(X(ω))/T_R)/Z$ for the recognition system with $T_R=1/β$ and partition function $Z=∑exp(−β J(X(ω')))$.
background
The module establishes J-cost as the ancestor of Shannon entropy by showing that the Gibbs weight arises as the unique maximizer of entropy subject to a fixed average J-cost constraint. J-cost is the functional $J(x)=(x+x^{-1})/2−1$ induced by the multiplicative recognizer on positive ratios; the associated cost of a recognition event is this J-value. Gibbs measure, partition function and recognition temperature $T_R$ are defined in RecognitionThermodynamics; the forward direction (Gibbs minimizes free energy) appears in MaxEntFromCost. The stationarity condition is the Euler-Lagrange equation for the Lagrangian $L=H(q)−β E(q)−λ(∑q−1)$ where $H$ is Shannon entropy and $E$ is average J-cost.
proof idea
From the given stationarity equation, exponentiate to obtain $q=exp(−β J−c)$. Factor the exponential and substitute into the sum-to-one hypothesis to isolate $exp(−c)=1/∑exp(−β J)$. Unfold the definitions of gibbs_measure, gibbs_weight and partition_function, substitute $T_R=1/β$, and simplify the exponent using field_simp on the relation $−J/T_R=−β J$. The final simp_rw step matches the normalized Gibbs weight term-by-term.
why it matters
This theorem supplies the converse direction to MaxEntFromCost: the exponential form is not postulated but forced by stationarity of the constrained entropy functional. It therefore closes the loop that derives $T_R$ as the Lagrange multiplier conjugate to average J-cost, consistent with the J-uniqueness property (T5) and the eight-tick octave structure. The result sits inside the ancestor hierarchy proving J-cost dominates squared-log information content, so Shannon entropy emerges only as the quadratic approximation. No downstream uses are recorded yet; the declaration remains a foundational bridge between ledger counting and thermodynamic potentials.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.