second_law
plain-language theorem explainer
The master statement of the second law in Recognition Science asserts that for any J-descent operator R fixing the Gibbs equilibrium peq of a recognition system, the discrete trajectory from any initial distribution q0 has non-increasing KL divergence to peq, non-increasing recognition free energy, and free energy bounded below by the equilibrium value. Researchers deriving thermodynamics from information geometry or cost functionals would cite this as the discrete Lyapunov function for recognition dynamics. The proof is a term-mode bundle that
Claim. Let $R$ be a J-descent operator on probability distributions over a finite space $Ω$ with fixed point the Gibbs measure $p_{eq}$ determined by recognition system $sys$ and cost function $X$. For any initial probability distribution $q_0$, the sequence $q_n = R^n q_0$ satisfies that the map $n ↦ D_{KL}(q_n ‖ p_{eq})$ is antitone, the map $n ↦ F_R(q_n)$ is antitone, and $F_R(q_n) ≥ F_R(p_{eq})$ for all natural numbers $n$.
background
A J-descent operator is a structure whose step map fixes the equilibrium distribution peq and satisfies KL non-increasing: for every distribution q, the KL divergence of step q to peq is at most that of q to peq. Recognition free energy $F_R(q)$ is the expected cost coordinate under q minus a temperature-scaled entropy term; its minimum is attained precisely at the Gibbs measure by the variational principle. The module works over a finite nonempty configuration space Ω equipped with a positive recognition temperature and a positive cost coordinate X, with gibbs_measure supplying the equilibrium distribution.
proof idea
The proof is a term-mode refinement constructing a triple. It invokes the lemma kl_divergence_antitone on R and q0, normalizes the first component via simpa using gibbsPD_p, then applies the exact lemmas free_energy_antitone and free_energy_ge_equilibrium for the remaining two properties.
why it matters
This theorem is the central result of the Thermodynamics.SecondLaw module and directly supplies the certificate used by secondLawCert_inhabited. It realizes the Lyapunov form in which $H_{RS}(q_n) := F_R(q_n) - F_R(p_{eq})$ is nonnegative and monotone non-increasing, furnishing the discrete second-law dynamics for the recognition operator. The result is consistent with the recognition composition law and the phi-ladder structure but remains agnostic to the concrete kernel realizing R.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.