max_ent_subject_to_cost
plain-language theorem explainer
The theorem shows that any probability distribution sharing the expected cost of the Gibbs measure cannot exceed the Gibbs measure in recognition entropy. Researchers deriving equilibrium states from variational principles in statistical mechanics would reference this when justifying the use of Gibbs ensembles. The argument reduces the entropy comparison to a free-energy inequality via substitution and applies non-linear arithmetic after confirming the temperature parameter is positive.
Claim. Let $p$ be a probability distribution on state space $Ω$ and let $X$ be the cost observable for system $sys$. If the expected cost of $p$ equals the expected cost of the Gibbs measure for $sys$ and $X$, then the recognition entropy of $p$ is at most the recognition entropy of the Gibbs measure.
background
This declaration belongs to the module that derives the Gibbs distribution as the maximum-entropy state under a fixed expected-cost constraint. Recognition entropy denotes the Shannon entropy of a distribution with respect to the recognition measure on $Ω$, while expected_cost computes the integral of the observable $X$ against the distribution. The recognition free energy is defined as expected cost minus temperature times entropy, with temperature supplied by the system parameter TR.
proof idea
The proof invokes the sibling lemma gibbs_minimizes_free_energy_basic on the input distribution $p$ to obtain a free-energy inequality. It unfolds the free-energy definition, substitutes the hypothesis that expected costs coincide, records positivity of the system temperature TR, and closes the resulting arithmetic comparison with nlinarith.
why it matters
The result supplies the maximum-entropy characterization of the Gibbs measure inside the Recognition Science thermodynamics layer. It completes the local derivation that equilibrium distributions follow from cost minimization alone. No downstream uses are recorded yet, but the statement aligns with the module goal of recovering thermodynamic relations from the underlying J-cost functional without external statistical postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.