h_theorem_recognition
plain-language theorem explainer
Recognition free energy decreases monotonically along any trajectory that relaxes toward the Gibbs measure. Information theorists and statistical mechanicians would cite this as the Recognition Science version of Boltzmann's H-theorem. The proof applies the variational identity F_R(p) = F_R(Gibbs) + T_R D_KL(p || Gibbs) twice, extracts the KL decrease from the relaxation hypothesis, and concludes via a non-positive product.
Claim. Let $sys$ be a recognition system, $X$ an observable, and $p(t)$ a family of distributions such that the Kullback-Leibler divergence from $p(t)$ to the Gibbs measure of $sys$ and $X$ is non-increasing in $t$. Then the recognition free energy satisfies $F_R(sys, p(t_2), X) ≤ F_R(sys, p(t_1), X)$ whenever $t_1 ≤ t_2$.
background
Recognition free energy obeys the identity $F_R(p) = F_R(Gibbs) + T_R D_{KL}(p || Gibbs)$, where $T_R$ is the recognition temperature and $D_{KL}$ is the Kullback-Leibler divergence; the Gibbs measure is the unique minimizer of $F_R$ for fixed observable $X$. The module proves that $F_R$ is non-increasing under RS dynamics (coarse-graining or relaxation), which is the Recognition Science counterpart to the second law. Upstream results supply the real-valued Energy type and the arithmetic and ledger structures that define the probability distributions and divergences.
proof idea
The proof invokes the free-energy-KL identity at both times, splits on whether $t_1 = t_2$, and otherwise extracts the KL decrease directly from the relaxation hypothesis via substitution. Algebraic rearrangement rewrites the target inequality as a product of the positive temperature factor and the non-positive KL difference; the product is shown non-positive by the mul_nonpos lemma.
why it matters
This supplies the relaxation half of the second-law statement in the Free Energy Monotonicity module and is recorded as proven in the module status report. It complements the coarse-graining result and directly supports the arrow-of-time definition via $dF_R/dt ≤ 0$. In the larger framework it realizes thermodynamic stability implied by the Recognition Composition Law and the forcing chain, closing one concrete step toward deriving the second law from T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.