gibbs_unique_minimizer
plain-language theorem explainer
The theorem establishes that any probability distribution attaining the same recognition free energy as the Gibbs measure must coincide with it at every state. Researchers deriving equilibrium distributions from cost minimization would cite this uniqueness when showing that the maximum-entropy state is the sole minimizer. The tactic proof applies the free-energy-KL identity to convert the equality hypothesis into vanishing KL divergence, then invokes the zero-KL characterization after using positivity of the recognition temperature.
Claim. Let $q$ be a probability distribution on a finite set $Ω$. If the recognition free energy of $q$ with respect to cost function $X$ equals the recognition free energy of the Gibbs measure $p_G$ associated to $X$, then $q(ω)=p_G(ω)$ for every $ω$. Here $p_G(ω)=exp(-X(ω)/T_R)/Z$ with $T_R$ the recognition temperature and $Z$ the partition function.
background
The module derives the Gibbs distribution as the unique solution to maximum entropy subject to a fixed average cost. A ProbabilityDistribution on $Ω$ is a nonnegative function summing to one. Recognition free energy is the functional $F_R(q)=⟨X⟩_q - T_R S(q)$, where $S$ denotes Shannon entropy. The Gibbs measure is the explicit distribution $p_G(ω)=exp(-X(ω)/T_R)/Z$ with $Z$ the normalizing constant.
proof idea
Apply free_energy_kl_identity to obtain that the free-energy difference equals $T_R$ times KL divergence. The equality hypothesis forces the left side to zero. Positivity of $T_R$ together with mul_eq_zero then implies the KL divergence vanishes. Finally apply kl_divergence_zero_iff_eq to conclude the distributions are identical.
why it matters
This supplies the uniqueness direction of the maximum-entropy principle. It is invoked directly by the bridge theorem gibbs_unique in JCostEntropyAncestor, which asserts that the Gibbs distribution is the unique free-energy minimizer and therefore the most probable macrostate. The result closes the derivation that cost minimization yields the exponential equilibrium form, aligning with the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.