free_energy_antitone
plain-language theorem explainer
Recognition free energy decreases monotonically along any trajectory generated by a J-descent operator on probability distributions. Researchers deriving thermodynamics from first principles in Recognition Science cite this result as the sharp Lyapunov form of the second law. The proof is a one-line wrapper that applies the ordering lemma free_energy_le_of_le after introducing the natural-number comparison hypothesis.
Claim. Let $sys$ be a recognition system, $X:Ω→ℝ$ a cost function, $R$ a J-descent operator fixing the Gibbs distribution $gibbsPD(sys,X)$, and $q_0$ an initial probability distribution. Then the sequence $n↦F_R(q_n)$ is antitone, where $q_n=R^n q_0$ and $F_R(q)$ denotes the recognition free energy of distribution $q$ with respect to $X$.
background
A JDescentOperator on distributions over finite Ω with equilibrium peq is a map step:DistribΩ→DistribΩ such that step(peq)=peq and KL divergence to peq is non-increasing under one application. The recognition free energy is the functional F_R(q)=∑q(ω)X(ω)+T_R D_KL(q‖gibbsPD(sys,X)) whose decrease encodes the second law. The module assembles the second law from the recognition operator projected onto the distribution layer, using the data-processing inequality for KL divergence as the canonical witness that any deterministic Markov kernel with stationary Gibbs measure satisfies the J-descent axioms.
proof idea
The proof is a one-line wrapper. It introduces the ordering hypothesis hnm:n≤m and hands the four arguments sys,X,R,q0 together with hnm directly to the lemma free_energy_le_of_le, which supplies the required inequality between the free-energy values at n and m.
why it matters
This theorem supplies the free-energy half of the master second_law bundle, which also contains the KL-divergence antitone statement and the variational lower bound by the Gibbs minimum. It realizes the Recognition Science claim that the recognition operator yields a Lyapunov function whose global minimum is the equilibrium distribution, thereby deriving the second law without new axioms. The result closes the discrete-time thermodynamics chain that begins from the J-cost definition and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.