JDescentOperator
plain-language theorem explainer
A J-descent operator abstracts recognition dynamics on probability distributions over finite Ω with equilibrium peq: it supplies a step map that fixes peq and keeps KL divergence to peq non-increasing. Researchers proving the second law from Recognition Science axioms cite this structure as the interface between the recognition operator and thermodynamic evolution. The definition is given directly as a structure whose two fields encode the fixed-point and non-expansiveness axioms.
Claim. A $J$-descent operator on probability distributions over a finite nonempty set $Ω$ with equilibrium distribution $p_{eq}$ consists of a map $step : P(Ω) → P(Ω)$ such that $step(p_{eq}) = p_{eq}$ and $D_{KL}(step(q) ‖ p_{eq}) ≤ D_{KL}(q ‖ p_{eq})$ for every distribution $q$.
background
The SecondLaw module derives the second law from Recognition Science first principles with zero sorrys. It introduces JDescentOperator peq as any step on distributions that fixes the Gibbs equilibrium peq = gibbsPD sys X (sys a RecognitionSystem, X a positive cost coordinate) and satisfies KL non-increase. This property holds for any deterministic Markov kernel with stationary peq via the data-processing inequality.
proof idea
The declaration is a structure definition. Its fields directly encode the fixed-point equation step peq = peq and the universal KL non-increase axiom. No lemmas or tactics are invoked; the structure serves as the type interface for downstream evolution and monotonicity results.
why it matters
JDescentOperator supplies the abstract dynamics used by free_energy_antitone to prove free energy is monotone non-increasing along trajectories and by entropy_increase_under_conservation for the entropy form under cost conservation. It realizes the module claim that the second law follows from the recognition operator. In the framework it links the J-cost function and discrete tick evolution to thermodynamic irreversibility, advancing the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.