kl_step_le
plain-language theorem explainer
Single-step contraction of Kullback-Leibler divergence holds for iteration of any J-descent operator. Workers deriving the second law from information geometry or recognition dynamics cite this when establishing monotonicity of free energy along discrete trajectories. The argument is a term-mode one-liner that rewrites the successor clause of the evolution map and applies the operator's built-in KL non-increase field.
Claim. Let $R$ be a J-descent operator with equilibrium distribution $p_{eq}$. For any initial distribution $q_0$ and natural number $n$, $D_{KL}((R. evolve (n+1) q_0).p || p_{eq}.p) ≤ D_{KL}((R. evolve n q_0).p || p_{eq}.p)$.
background
A J-descent operator on probability distributions over finite Ω with equilibrium peq is a structure whose step map fixes peq and obeys KL non-expansiveness: the divergence to peq never increases under one application of the step. The evolve function iterates this step recursively, with evolve 0 q defined as q itself and evolve (n+1) q defined as R.step applied to the result at n. KL divergence is the standard sum q(ω) log(q(ω)/p(ω)) over states where both are positive.
proof idea
The proof is a term-mode one-liner. It rewrites the left-hand side via the evolve_succ lemma, which unfolds evolve (n+1) q to R.step (evolve n q), then applies the kl_non_increasing field of the JDescentOperator structure directly to the distribution obtained after n steps.
why it matters
This single-step contraction is invoked inside free_energy_step_le to transfer the inequality to recognition free energy and inside kl_le_of_le to obtain the full n ≤ m monotonicity by induction. It supplies the base case for the second-law statements in the module, connecting the abstract J-descent property of the recognition operator to monotonic decrease of free energy toward the Gibbs equilibrium.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.