module module high

`IndisputableMonolith.Thermodynamics.FreeEnergyMonotone`

FreeEnergyMonotone establishes monotonicity of free energy under coarse graining and derives an H-theorem for Recognition Science dynamics. Researchers modeling memory retention or error correction in RS thermodynamics cite its inequalities to obtain the arrow of time from the J-cost. The argument proceeds from convexity of x log x through log-sum and data-processing inequalities to the final monotonicity statements.

claimThe function $f(x) = x log x$ is convex on $(0,∞)$, which implies that the free-energy functional $F$ satisfies $F(μ) ≥ F(ν)$ whenever $ν$ is a coarse-graining of the measure $μ$ in the Recognition cost model.

background

Recognition Science begins from the T=0 cost functional $J(x) = ½(x + x^{-1}) - 1$ whose absolute minimum defines the ground state. The upstream MaxEntFromCost module shows that the Gibbs distribution arises by maximizing entropy subject to a fixed expected cost. FreeEnergyMonotone extends this setting by adjoining the Shannon entropy term to produce a free-energy functional and then studies its behavior under measure transformations.

proof idea

The module first records the convexity of $x log x$ on the positive reals. It then derives the log-sum inequality and the push-forward preservation properties, applies them to obtain the data-processing inequality, and finally shows that coarse graining strictly decreases free energy, yielding the recognition H-theorem and arrow-of-time statements.

why it matters in Recognition Science

The module supplies the monotonicity and H-theorem ingredients required by the parent Thermodynamics module. It also feeds ErrorCorrection by bounding defect growth under coarse graining and MemoryLedger by quantifying free-energy decay during memory retention. It thereby converts the static J-minimization principle into an explicit irreversible dynamics within the Recognition framework.

scope and limits

Does not treat continuous-time flows or differential equations.
Does not incorporate quantum statistics or entanglement.
Does not compute explicit numerical values for specific physical systems.
Does not address relativistic or gravitational corrections to J.

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Thermodynamics module_import
IndisputableMonolith.Thermodynamics.ErrorCorrection module_import
IndisputableMonolith.Thermodynamics.MemoryLedger module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Thermodynamics.MaxEntFromCost module_import

declarations in this module (13)

lemma mul_log_convexOn L36
theorem log_sum_inequality L68
theorem log_sum_inequality_fiber L113
def push_forward L156
theorem push_forward_nonneg L160
theorem push_forward_sum_one L169
def effective_cost L179
theorem partition_function_preserved L189
theorem data_processing_inequality L236
theorem coarse_graining_decreases_free_energy L324
def rs_arrow_of_time L381
theorem h_theorem_recognition L398
def free_energy_monotone_status L431