evolve
plain-language theorem explainer
The iterated evolution operator under a J-descent operator R, which fixes the equilibrium distribution and contracts KL divergence to it, is defined recursively by applying the single step n times. Researchers formalizing thermodynamic trajectories in Recognition Science cite this construction to generate discrete sequences for monotonicity arguments. It is realized as a direct recursive case split on the iteration count.
Claim. Let $peq$ be a probability distribution on a finite set $Ω$. For a J-descent operator $R$ relative to $peq$, the iterated map $E: ℕ × 𝒫(Ω) → 𝒫(Ω)$ satisfies $E(0, q) = q$ and $E(n+1, q) = R.step(E(n, q))$.
background
A ProbabilityDistribution on $Ω$ is a nonnegative function summing to one. The JDescentOperator structure on $peq$ supplies a step map that fixes $peq$ and obeys KL non-increase: $D_{KL}(step q ‖ peq) ≤ D_{KL}(q ‖ peq)$. The module sets this as the abstract recognition operator $R̂$ on distributions, with any Markov kernel having $peq$ stationary satisfying the axioms via the data-processing inequality.
proof idea
The definition is a recursive case distinction on the natural number: the zero case returns the input distribution unchanged, while the successor case composes one application of the step operator onto the result of the prior iteration.
why it matters
This supplies the discrete trajectory $q_n$ used to prove KL antitone and free-energy antitone in the same module, establishing the second law. It is invoked in downstream results including eight_tick_dissipation_limit and main_resolution. Within the framework it realizes the eight-tick octave at the distribution layer, linking recognition steps to the composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.