secondLawCert
plain-language theorem explainer
secondLawCert constructs the master certificate SecondLawCert by supplying proofs for its fields from KL non-negativity and free energy lemmas. Researchers formalizing thermodynamics in recognition-based models cite it to obtain a single inhabited record containing Gibbs inequality, variational principle, and monotonicity statements. The definition is a direct structure builder invoking upstream results on divergence and free energy without new hypotheses.
Claim. For a RecognitionSystem $sys$ and cost function $X:Ω→ℝ$, the certificate $secondLawCert(sys,X)$ is the structure containing the non-negativity of the Kullback-Leibler divergence to the Gibbs measure $π=gibbs_measure(sys,X)$, the minimization of recognition free energy at $π$, the identity relating free energy difference to $T_R$ times KL divergence, and the monotonicity of KL divergence, free energy, and entropy (under conservation) along trajectories of any J-descent operator.
background
The module derives the second law from the recognition operator's J-descent property on probability distributions over a finite configuration space $Ω$. A RecognitionSystem fixes the recognition temperature $T_R>0$, and the Gibbs measure is defined by $π(ω)=exp(-J(X(ω))/T_R)/Z$, where $J$ is the recognition cost function. A JDescentOperator $R$ fixes the equilibrium $π$ and satisfies $D_{KL}(R q ‖ π)≤D_{KL}(q ‖ π)$ for all $q$ (MODULE_DOC). Upstream results include the free energy-KL identity: $F_R(q)-F_R(Gibbs)=T_R D_{KL}(q ‖ Gibbs)$ (free_energy_kl_identity) and the non-negativity of KL divergence (kl_divergence_nonneg).
proof idea
The definition populates the SecondLawCert record directly. The gibbs_inequality field applies kl_divergence_nonneg to the Gibbs measure with the required positivity and normalization conditions. gibbs_minimizes invokes gibbs_minimizes_free_energy_basic. The fe_kl_identity field uses free_energy_kl_identity. kl_monotone reduces via simpa to kl_divergence_antitone after unfolding gibbsPD_p. free_energy_monotone applies free_energy_antitone, and the entropy field applies second_law_entropy_form under the conservation hypothesis.
why it matters
This definition supplies the concrete inhabitant for SecondLawCert, which is immediately used by secondLawCert_inhabited to prove the certificate is nonempty for every sys and X. It assembles the full set of second-law statements (free energy decrease along J-descent trajectories, entropy increase under conservation) from the RecognitionThermodynamics and MaxEntFromCost modules, completing the derivation of the second law from the J-uniqueness and self-similar fixed point in the forcing chain. It leaves open the extension to infinite or continuous state spaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.