evolve_zero
plain-language theorem explainer
The lemma establishes that zero iterations of any J-descent operator leave an arbitrary initial probability distribution unchanged. Researchers formalizing discrete thermodynamic trajectories and the second law in Recognition Science cite it as the base case for inductive arguments on KL divergence and free energy. The proof is a direct reflexivity reduction after omitting the nonemptiness hypothesis on the configuration space.
Claim. Let $p_{eq}$ be a probability distribution on a finite set $Ω$. Let $R$ be a J-descent operator with fixed point $p_{eq}$, so that $R(p_{eq})=p_{eq}$ and the Kullback-Leibler divergence from any distribution $q$ to $p_{eq}$ does not increase under one application of $R$. Then the zero-step evolution satisfies $R^0 q = q$.
background
ProbabilityDistribution is the structure of a function $p:Ω→ℝ$ that is nonnegative everywhere and sums to one over the finite set $Ω$. JDescentOperator $p_{eq}$ packages a step map from distributions to distributions together with the two axioms that the step fixes $p_{eq}$ and never increases KL divergence to $p_{eq}$. The evolve map is the discrete iteration of this step: it returns the input at count zero and applies the step to the result of the preceding count otherwise. The surrounding module derives the second law by showing that any such operator produces monotone descent of free energy along its trajectories.
proof idea
One-line wrapper that applies reflexivity to the base clause of the recursive definition of evolve.
why it matters
The result supplies the base case required by the inductive proofs of kl_divergence_antitone and free_energy_antitone inside the same module. Those statements in turn deliver the second-law bundle (monotone free-energy descent, variational inequality, and entropy increase under conserved mean cost) that the module presents as the Recognition Science derivation of the classical second law. It closes the zero-tick edge of the discrete trajectory construction without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.