kl_le_of_le
plain-language theorem explainer
The theorem shows that for any J-descent operator R fixing equilibrium peq, KL divergence from the evolved state at step m is at most the divergence at step n whenever n ≤ m. Thermodynamic derivations in Recognition Science cite this monotonicity to obtain the second law in KL form before scaling to free energy. The proof is a direct induction on the natural-number inequality, applying the single-step contraction at each successor and reflexivity at the base.
Claim. Let $R$ be a J-descent operator on probability distributions over finite nonempty space $Ω$ with fixed equilibrium $p_{eq}$. For any initial distribution $q_0$ and natural numbers $n ≤ m$, the Kullback-Leibler divergence satisfies $D_{KL}(R^m q_0 ‖ p_{eq}) ≤ D_{KL}(R^n q_0 ‖ p_{eq})$.
background
A J-descent operator on distributions over $Ω$ is a map that fixes the equilibrium distribution $p_{eq}$ and satisfies the single-step KL non-expansion $D_{KL}(R q ‖ p_{eq}) ≤ D_{KL}(q ‖ p_{eq})$ for every $q$. The module assembles the second law by showing that iterated application of any such operator produces a monotone non-increasing sequence of divergences to equilibrium. This rests on the single-step contraction (kl_step_le) together with the arithmetic lemmas le_refl and le_trans for the order on natural numbers.
proof idea
The proof is by induction on the hypothesis $n ≤ m$. The base case (refl) invokes le_refl. The successor case applies kl_step_le to obtain the one-step contraction and then chains the resulting inequality to the inductive hypothesis via le_trans.
why it matters
This lemma supplies the key monotonicity step for kl_divergence_antitone, which the module describes as the deepest single inequality in the second-law derivation; the free-energy version follows by one multiplication. It closes the KL part of the second-law bundle inside the Recognition Science framework, linking the abstract J-descent operator directly to the classical entropy non-decrease under conserved energy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.