module module high

`IndisputableMonolith.Thermodynamics.SecondLaw`

This module packages the Gibbs measure as a ProbabilityDistribution to serve as the equilibrium reference for J-descent dynamics. It imports the cost function and maximum-entropy results to define the fixed point under Recognition Temperature. The module supplies the reference state needed for thermodynamic evolution arguments in Recognition Science. It contains no proofs and consists of definitions plus supporting lemmas.

claimThe central object is the Gibbs probability distribution $\mathrm{GibbsPD}$ obtained by maximizing entropy subject to a fixed $J$-cost constraint, acting as the equilibrium measure for the evolution operator under finite Recognition Temperature $T_R$.

background

Recognition Science extends $T=0$ cost minimization to finite Recognition Temperature $T_R$ in the RecognitionThermodynamics module. The upstream MaxEntFromCost result establishes that the Gibbs distribution arises as the unique maximum-entropy state under a $J$-cost constraint. The present module packages that distribution as a ProbabilityDistribution to serve as the reference state for J-descent dynamics.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the equilibrium reference required by the J-descent operator and free-energy lemmas listed among its siblings. It therefore feeds the formulation of the second law within the Recognition Thermodynamics framework.

scope and limits

Does not prove the second-law inequality.
Does not treat time-dependent or non-equilibrium trajectories.
Does not derive numerical values for $T_R$ or the Gibbs measure.
Does not address interactions beyond the single-system cost constraint.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Thermodynamics.MaxEntFromCost module_import
IndisputableMonolith.Thermodynamics.RecognitionThermodynamics module_import

declarations in this module (22)

def gibbsPD L110
lemma gibbsPD_p L116
structure JDescentOperator L132
def evolve L145
lemma evolve_zero L152
lemma evolve_succ L157
theorem evolve_equilibrium_eq L163
theorem kl_step_le L177
theorem kl_le_of_le L186
theorem kl_divergence_antitone L199
lemma fe_kl_id L207
theorem free_energy_step_le L216
theorem free_energy_le_of_le L231
theorem free_energy_antitone L245
theorem free_energy_ge_equilibrium L253
theorem second_law L273
theorem second_law_one_statement L300
theorem second_law_entropy_form L334
theorem entropy_increase_under_conservation L355
structure SecondLawCert L374
def secondLawCert L406
theorem secondLawCert_inhabited L422