module module moderate

`IndisputableMonolith.Thermodynamics.SecondLaw`

The SecondLaw module packages the Gibbs measure as a ProbabilityDistribution. It supplies the equilibrium reference for J-descent dynamics within Recognition Science thermodynamics. The module imports Cost, MaxEntFromCost, and RecognitionThermodynamics to establish this reference point for descent operators.

claimThe Gibbs measure is packaged as a ProbabilityDistribution $P$ that serves as the equilibrium reference for the J-descent dynamics.

background

RecognitionThermodynamics extends zero-temperature cost minimization (J=0) to finite Recognition Temperature TR. MaxEntFromCost proves that the Gibbs distribution emerges from maximum entropy subject to a cost constraint. The Cost module supplies the underlying J-cost function. This module packages that Gibbs measure as a ProbabilityDistribution for use in J-descent dynamics.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the equilibrium reference for J-descent dynamics and supports the second law in Recognition Science. It connects directly to the maximum-entropy derivation in MaxEntFromCost and the finite-temperature extension in RecognitionThermodynamics.

scope and limits

Does not derive the second law of thermodynamics.
Does not define the explicit form of the J-cost function.
Does not implement numerical simulation of descent trajectories.
Does not address multi-particle or interacting systems.

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