pith. sign in
module module high

IndisputableMonolith.Thermodynamics.MaxEntFromCost

show as:
view Lean formalization →

The MaxEntFromCost module derives the maximum-entropy principle as a theorem of constrained J-cost minimization at finite Recognition Temperature. Researchers connecting Recognition Science to statistical mechanics cite these identities when moving from T=0 cost functionals to thermodynamic potentials. The arguments consist of direct algebraic expansions of the free-energy functional together with substitution of the Gibbs form.

claim$F_R(q) - F_R(p) = T_R D_{KL}(q || p)$ where $p$ is the Gibbs distribution minimizing $F_R$, $F_R(q) = ⟨X⟩_q - T_R S(q)$, and $D_{KL}$ is the Kullback-Leibler divergence.

background

RecognitionThermodynamics extends the absolute J-minimization of the Cost module to finite Recognition Temperature $T_R$, which controls the softness of the constraint. The free-energy functional is defined as the Legendre transform of the entropy subject to the expected cost constraint. The module supplies the algebraic identities that convert this constrained optimization into an unconstrained minimum of $F_R$.

proof idea

The central identity is proved by expanding $F_R(q)$ into its expectation and entropy terms, inserting the explicit form log p_ω = -X_ω/T_R - log Z for the Gibbs state, and rearranging the resulting expression into the KL divergence. The remaining sibling theorems (Gibbs minimizes free energy, KL zero iff equality) are immediate corollaries of the same expansion.

why it matters in Recognition Science

The identities feed directly into FreeEnergyMonotone (monotonicity of F_R under RS dynamics) and SecondLaw (the second-law statement from first principles). They also supply the thermodynamic bridge used by JCostEntropyAncestor to show that the Gibbs weight is a derived theorem rather than an axiom.

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)