evolve_equilibrium_eq
plain-language theorem explainer
Equilibrium distributions remain invariant under any finite number of iterations of a J-descent operator. Researchers deriving the second law from recognition first principles cite this stationarity to anchor the variational principle and free-energy descent. The proof is a direct induction on iteration count that applies the successor evolution rule together with the operator's fixed-point property.
Claim. Let $p_{eq}$ be a probability distribution on a finite nonempty set $Ω$. Let $R$ be a J-descent operator for $p_{eq}$, so $R(p_{eq})=p_{eq}$ and $D_{KL}(R(q)‖p_{eq})≤D_{KL}(q‖p_{eq})$ for every distribution $q$. Then the $n$-fold iterate satisfies $R^n(p_{eq})=p_{eq}$ for every natural number $n$.
background
A J-descent operator on distributions over $Ω$ with equilibrium $p_{eq}$ consists of a single-step map that fixes $p_{eq}$ and is non-expansive in Kullback-Leibler divergence to $p_{eq}$. This structure abstracts the recognition operator projected onto the probability layer inside Recognition Science. The module assembles the second law by proving that free energy is monotone non-increasing along trajectories generated by any such operator, with equilibrium as the global minimum.
proof idea
The argument is an induction on $n$. The zero case holds by reflexivity. The successor case rewrites the iterated evolution via the successor rule, substitutes the inductive hypothesis, and applies the fixed-point property of the operator to obtain equality after simplification.
why it matters
The result supplies the stationarity needed for the variational inequality and monotonicity statements that constitute the second law in this module. It confirms that the Gibbs equilibrium is a fixed point of the recognition dynamics, consistent with the J-cost and recognition composition law. No open questions remain inside the proved fragment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.