entropy_increase_under_conservation
plain-language theorem explainer
The theorem establishes that recognition entropy is non-decreasing along trajectories generated by any J-descent operator whenever expected cost is conserved. Researchers deriving the second law from information geometry or first-principles recognition operators would cite this result. The proof is a one-line wrapper that applies the entropy monotonicity lemma and finishes with linear arithmetic.
Claim. Let $sys$ be a recognition system, $X : Ω → ℝ$ a cost function, $R$ a J-descent operator fixing the Gibbs distribution $π = gibbsPD(sys, X)$, and $q_0$ an initial probability distribution. If expected cost is conserved, i.e., $ℰ_{q_n}[X] = ℰ_{q_0}[X]$ for the orbit $q_n = R^n q_0$, then for integers $n ≤ m$ the recognition entropy satisfies $S_R(q_m) ≥ S_R(q_n)$.
background
The module derives the second law inside Recognition Science from the J-descent property with zero axioms or sorrys. A JDescentOperator on distributions over finite nonempty Ω fixes the equilibrium Gibbs measure π and is non-expansive in KL divergence: $D_{KL}(R q ‖ π) ≤ D_{KL}(q ‖ π)$. The recognition operator projected to the distribution layer supplies the canonical example via the data-processing inequality. Under this operator the discrete trajectory is $q_n = R^n q_0$. When the expected cost $⟨X⟩$ is conserved along the trajectory, the module proves monotonicity of recognition entropy $S_R(q_n)$.
proof idea
The proof applies the lemma second_law_entropy_form to obtain recognition_entropy (R.evolve m q₀).p ≥ recognition_entropy (R.evolve n q₀).p under the given conservation hypothesis and the ordering n ≤ m, then concludes with linarith.
why it matters
This supplies the classical numeric ΔS ≥ 0 form of the second law under energy conservation and completes the master certificate that bundles every classical statement provable from J-descent. It realizes the entropy-increase statement that follows from KL non-expansiveness once the cost coordinate is conserved, placing the Clausius form inside the Recognition Science derivation of thermodynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.