second_law_entropy_form
plain-language theorem explainer
If expected J-cost remains invariant along trajectories of a J-descent operator, recognition entropy is monotone non-decreasing in the discrete time index. Recognition Science derivations of thermodynamics cite this as the entropy form of the second law for isolated systems. The argument substitutes the conservation hypothesis into the already-proved free-energy decrease and rearranges via positivity of the recognition temperature.
Claim. Let $sys$ be a recognition system with positive recognition temperature $T_R$, let $X : Ω → ℝ$ assign costs, let $R$ be a J-descent operator fixing the Gibbs distribution $π = gibbsPD(sys,X)$, and let $q_0$ be an initial probability distribution. If expected cost is conserved, i.e., $E_{q_n}[X] = E_{q_0}[X]$ for every iterate $q_n = R^n q_0$, then the recognition entropy $S_R(q_n) = -∑ q_n(ω) log q_n(ω)$ is a non-decreasing function of $n$.
background
A J-descent operator on distributions over finite Ω is a map that fixes the equilibrium Gibbs distribution and satisfies KL non-expansiveness to that equilibrium. Recognition entropy is the Shannon entropy $S_R(q) = -∑ q(ω) log q(ω)$. Recognition free energy is the variational quantity $F_R(q) = E_q[J(X)] - T_R S_R(q)$, where expected cost is the sum $∑ p(ω) J(X(ω))$ and $T_R > 0$ is fixed by the recognition system.
proof idea
The proof introduces the free-energy inequality at steps n and m supplied by the upstream lemma free_energy_le_of_le. It applies the conservation hypothesis to equate the expected-cost terms, unfolds the definition of recognition free energy, rewrites, and concludes the entropy comparison by nlinarith using the positivity fact sys.TR_pos.
why it matters
The result supplies the classical Clausius statement ΔS ≥ 0 inside Recognition Science and feeds the numeric increase theorem entropy_increase_under_conservation together with the master certificate secondLawCert. It completes the module's derivation of the second law from the J-cost functional and J-descent structure with zero axioms, consistent with the free-energy variational principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.