module module moderate

`IndisputableMonolith.Thermodynamics.SecondLaw`

Module packages the Gibbs measure as a ProbabilityDistribution to serve as the equilibrium reference for J-descent dynamics. Researchers in Recognition Thermodynamics cite it when modeling finite-temperature equilibria derived from cost minimization. The module assembles this reference by importing the Gibbs form from MaxEntFromCost and the Recognition Temperature parameterization from RecognitionThermodynamics.

claimThe Gibbs measure is packaged as a probability distribution $P$ on the configuration space that maximizes entropy subject to a fixed average J-cost constraint at recognition temperature $T_R$.

background

Recognition Science extends zero-temperature cost minimization to finite Recognition Temperature $T_R$ in the RecognitionThermodynamics module, where $T_R$ parameterizes the strictness of J-minimization. MaxEntFromCost proves that the Gibbs distribution emerges from the principle of maximum entropy subject to a cost constraint. The Cost module supplies the underlying J-cost function. This module sits in the Thermodynamics domain and packages the resulting distribution as the reference equilibrium for J-descent dynamics.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Supplies the equilibrium reference required for J-descent dynamics and free-energy constructions in the Second Law setting. It feeds the sibling definitions of JDescentOperator, evolve, and free_energy_step_le. The module connects the maximum-entropy result to the finite-temperature extension of Recognition Thermodynamics.

scope and limits

Does not derive any second-law inequality.
Does not specify explicit forms for the J-cost function.
Does not compute numerical values of recognition temperature.
Does not address non-equilibrium dynamics beyond the reference state.

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