SecondLawCert
plain-language theorem explainer
SecondLawCert bundles the Gibbs inequality, variational principle, free-energy/KL identity, and monotonicity of both KL divergence and free energy under any J-descent operator, plus entropy increase when expected cost is conserved. A physicist deriving thermodynamic inequalities from information geometry would cite this record to obtain all standard second-law forms from the single J-descent axiom. The declaration is a pure structure definition whose five fields are the bundled statements; the actual verifications appear in the companion second
Claim. Let Ω be finite and nonempty, sys a RecognitionSystem with temperature T_R > 0, X : Ω → ℝ a positive cost function, and π the Gibbs measure gibbs_measure(sys, X). A certificate consists of: (i) D_KL(q ‖ π) ≥ 0 for every probability distribution q; (ii) recognition_free_energy(sys, π, X) ≤ recognition_free_energy(sys, q, X); (iii) recognition_free_energy(sys, q, X) − recognition_free_energy(sys, π, X) = T_R · D_KL(q ‖ π); (iv) for any J-descent operator R fixing π the map n ↦ D_KL(R^n q ‖ π) is antitone; (v) the map n ↦ recognition_free_energy(sys, R^n q, X) is antitone; (vi) when expected_cost is conserved along the trajectory, recognition_entropy(R^n q) is monotone non-decreasing.
background
The module derives the second law from the J-descent property of the recognition operator. A JDescentOperator on distributions with equilibrium π is a map step that fixes π and satisfies D_KL(step q ‖ π) ≤ D_KL(q ‖ π) for every q; this is the abstract form of the recognition operator projected onto the probability layer. The upstream entropy definition states that entropy of a configuration is proportional to its total defect, with zero defect giving the minimum-entropy state. The module documentation records that any deterministic Markov kernel with π as stationary distribution satisfies the J-descent axioms via the data-processing inequality.
proof idea
This is a structure definition. It declares the five fields as the required properties with no computational body. The verifications that the properties hold are supplied by the constructor secondLawCert, which invokes kl_divergence_nonneg together with the antitone results from the free-energy module.
why it matters
This certificate is the central object used by secondLawCert and secondLawCert_inhabited to witness that the second law holds inside Recognition Science. It directly implements the statements listed in the module documentation: KL and free-energy antitone along J-descent, the variational principle, and entropy increase under energy conservation. In the broader framework it closes the thermodynamics section by showing that the J-cost operator alone forces the second law, consistent with the forcing chain from T5 onward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.