Pith. sign in
module module high

IndisputableMonolith.Thermodynamics.MaxEntFromCost

show as:
view Lean formalization →

This module derives the maximum entropy principle from the Recognition cost functional at finite temperature. It proves that the excess free energy of any distribution q equals TR times its KL divergence from the Gibbs state. Researchers in statistical mechanics foundations cite it to obtain the equilibrium distribution as a theorem rather than an assumption. The argument consists of algebraic expansion of the free energy and divergence definitions.

claim$F_R(q) - F_R(p_{\text{Gibbs}}) = T_R \, D_{KL}(q \| p_{\text{Gibbs}})$ where $p_{\text{Gibbs},\omega} = \exp(-X_\omega / T_R) / Z$ minimizes the Recognition free energy at temperature $T_R$.

background

Recognition Science begins with T=0 minimization of the cost J(x) = (x + x^{-1})/2 - 1. The RecognitionThermodynamics module extends this to finite Recognition Temperature TR that parametrizes the strictness of J-minimization. MaxEntFromCost imports the cost definitions and works inside that finite-temperature setting to obtain the maximum-entropy distribution as the unique free-energy minimizer.

proof idea

The module assembles several results around the free-energy KL identity. The identity is obtained by direct substitution of the Gibbs form log p = -X/TR - log Z into the KL sum, followed by rearrangement that isolates the free-energy difference. Companion results establish uniqueness of the minimizer and the zero-divergence case.

why it matters in Recognition Science

The module supplies the identity that downstream modules use to prove free-energy monotonicity and the second law. It feeds IndisputableMonolith.Thermodynamics.FreeEnergyMonotone and IndisputableMonolith.Thermodynamics.SecondLaw. The result realizes the Gibbs weight exp(-J/TR) as a theorem of constrained optimization on many-body ledgers rather than a postulate.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (5)