entropy_maximizer_is_gibbs
plain-language theorem explainer
The theorem shows that the Gibbs measure built from J-cost ratios on a many-body ledger minimizes recognition free energy among all distributions on K states. Workers deriving thermodynamic structure from constrained counting in recognition systems would cite it to justify the exponential form. The tactic proof obtains a nonempty instance for Fin K and applies the basic minimization lemma in one step.
Claim. Let $p$ be the Gibbs measure on the finite set of $K$ states whose costs are the ledger ratios. Then for every probability distribution $q$ on those states, the recognition free energy of $p$ is at most the recognition free energy of $q$.
background
A ManyBodyLedger K is a structure recording M positive subsystems and K positive real ratios that serve as J-costs. The recognition free energy is the expected J-cost minus a temperature factor times Shannon entropy. The module derives this functional by maximizing the multinomial microstate count subject to fixed average J-cost, using Lagrange multipliers to obtain the exponential weights. Upstream results supply the entropy definition as total defect and the J-cost as the derived cost of a multiplicative recognizer.
proof idea
The tactic proof first constructs a Nonempty instance for Fin K from the positivity hypothesis. It then introduces the two distributions and reduces the claim by direct application of the lemma gibbs_minimizes_free_energy_basic on the system and the ratio function.
why it matters
This result establishes that the free-energy functional and the Gibbs distribution are forced by counting microstates under a J-cost constraint, rather than postulated. It completes the backward direction in the module's ancestor hierarchy, where J-cost dominates squared log and Shannon entropy appears only as a quadratic approximation. The declaration sits between the basic minimization lemma and the temperature-as-Lagrange-multiplier statement in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.