JDescentOperator
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.
claimA $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 in Recognition Science
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.
scope and limits
- Does not construct any concrete step map.
- Does not prove existence of such operators.
- Does not address continuous-time limits.
- Does not treat infinite or quantum state spaces.
formal statement (Lean)
132structure JDescentOperator (peq : ProbabilityDistribution Ω) where
133 /-- The single-tick recognition step on probability distributions. -/
134 step : ProbabilityDistribution Ω → ProbabilityDistribution Ω
135 /-- Equilibrium is a fixed point. -/
136 fixes_equilibrium : step peq = peq
137 /-- KL divergence to equilibrium does not increase under one tick. -/
138 kl_non_increasing :
139 ∀ q : ProbabilityDistribution Ω,
140 kl_divergence (step q).p peq.p ≤ kl_divergence q.p peq.p
141
142namespace JDescentOperator
143
144/-- Discrete iteration of a J-descent operator. -/