gibbs_unique
plain-language theorem explainer
The declaration establishes that any probability distribution achieving the same recognition free energy as the Gibbs measure for a given cost function X must coincide with that Gibbs measure. A researcher deriving thermodynamic distributions from constrained J-cost optimization on many-body systems would cite it to justify uniqueness of the Boltzmann form. The proof is a direct one-line application of the free-energy minimizer uniqueness result.
Claim. Let $sys$ be a recognition system, $X:Ω→ℝ$ a cost function, and $q$ a probability distribution on $Ω$. If the recognition free energy of $q$ under $sys$ and $X$ equals the recognition free energy of the Gibbs measure induced by $sys$ and $X$, then $q$ equals the Gibbs measure pointwise.
background
The J-cost functional $J(x)=½(x+x^{-1})-1$ is the energy measure induced by multiplicative recognizers and recognition events. The module shows that, for many independent subsystems with fixed average J-cost, the most probable macrostate maximizes Shannon entropy subject to the cost constraint; Lagrange multipliers then force the Gibbs weights $p_i^*=exp(-J(r_i)/T_R)/Z$ with $T_R$ derived as the multiplier. This theorem supplies the uniqueness half of that derivation: equality of free energies implies identity with the Gibbs form. Upstream results establish that cost is nonnegative and derived directly from recognition comparators.
proof idea
The proof is a one-line wrapper that applies the uniqueness lemma for free-energy minimizers to the given equality of recognition free energies, yielding pointwise equality of the distributions.
why it matters
This is Bridge Theorem 2, closing the uniqueness direction in the J-cost to entropy derivation. It combines with the multinomial counting argument to identify the most probable macrostate with the Gibbs distribution, showing that the Boltzmann form is forced by optimization rather than postulated. In the Recognition Science chain it links J-cost optimization (T5 J-uniqueness) to thermodynamic structures, with $T_R$ emerging from the Lagrange multiplier and Shannon entropy appearing as the quadratic shadow of J-cost. No downstream uses are recorded in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.