evolve_succ
plain-language theorem explainer
The successor recursion for the iterated J-descent operator holds by definition of the evolution map. Researchers proving the second law via monotonicity of KL divergence or free energy cite this to handle the inductive step in trajectory arguments. The proof reduces immediately to reflexivity once the recursive clause of evolve is unfolded.
Claim. Let $R$ be a J-descent operator on probability distributions over a finite space $Ω$ with equilibrium $p_{eq}$. For any natural number $n$ and distribution $q$, the iterated application satisfies $R^{n+1} q = R(R^n q)$.
background
In the Recognition Science treatment of thermodynamics, a J-descent operator $R$ on distributions over a finite configuration space $Ω$ consists of a step map that fixes the equilibrium $p_{eq}$ and contracts KL divergence to it: step $p_{eq} = p_{eq}$ and $D_{KL}$(step $q$ || $p_{eq}$) ≤ $D_{KL}$($q$ || $p_{eq}$). The module proves the second law by showing that iterated application of any such operator yields monotone decrease in free energy and KL divergence along trajectories $q_n = R^n q_0$. This lemma supplies the recursive unfolding needed for induction on the number of steps.
proof idea
The proof is a one-line wrapper that applies the recursive definition of the evolve function on JDescentOperator.
why it matters
This lemma is invoked directly in the proofs of evolve_equilibrium_eq and kl_step_le, which establish that the equilibrium is a fixed point and that KL divergence decreases at each step. It supports the second-law statement in the module by enabling the inductive argument that free energy is antitone along trajectories. Within the framework it closes the discrete-time iteration for the recognition operator R̂ projected to distributions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.