pith. sign in
module module high

IndisputableMonolith.Thermodynamics.MaxEntFromCost

show as:
view Lean formalization →

MaxEntFromCost derives the maximum-entropy principle from Recognition free-energy minimization at finite T_R. Researchers building the second law or free-energy monotonicity in Recognition Science cite the KL identity and its corollaries. The proofs are direct algebraic substitutions of the Gibbs weights into the definitions of F_R and D_KL, with no additional axioms.

claim$F_R(q) - F_R(p) = T_R D_{\mathrm{KL}}(q \| p)$ where $p_\omega = \exp(-X_\omega / T_R)/Z$ is the Gibbs minimizer of $F_R(q) = \langle X \rangle_q - T_R S(q)$.

background

RecognitionThermodynamics extends the T=0 absolute minimization of the J-functional to finite Recognition Temperature T_R that parameterizes the strictness of cost minimization. The imported Cost module supplies the underlying J-cost. The present module works with the Recognition free energy F_R(q) and the associated Gibbs state.

The parent Thermodynamics module states the T=0 foundation: reality is defined by absolute minimization of J(x) = ½(x + 1/x) - 1. All results here are obtained inside that statistical-mechanics extension.

proof idea

The central free-energy–KL identity is obtained by substituting the explicit Gibbs form p_ω = exp(−X_ω/T_R)/Z into the definitions of F_R and D_KL and rearranging. The remaining siblings (max_ent_subject_to_cost, gibbs_unique_minimizer, kl_divergence_zero_iff_eq) are immediate corollaries of the same variational equality. The module is therefore a collection of algebraic identities.

why it matters in Recognition Science

The identities are imported by FreeEnergyMonotone to prove non-increasing F_R under RS dynamics, by JCostEntropyAncestor to derive the J-cost–entropy bridge, and by SecondLaw to obtain the second-law theorem with zero sorry. The module therefore supplies the variational step that converts cost minimization into thermodynamic potentials inside Recognition Science.

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)