second_law_one_statement
plain-language theorem explainer
The declaration proves that the excess recognition free energy H(n) = F_R(R^n q0) - F_R(gibbs equilibrium) is nonnegative for every n and strictly antitone along any J-descent trajectory. Researchers deriving the second law from recognition primitives would cite this as the Lyapunov form of the RS second law. The proof is a direct two-part split that invokes the variational inequality free_energy_ge_equilibrium for the lower bound and the monotonicity lemma free_energy_le_of_le for the antitone property, both discharged by linarith.
Claim. Let sys be a recognition system, X : Ω → ℝ a cost function, R a J-descent operator fixing the Gibbs equilibrium π = gibbs_measure(sys, X), and q₀ an initial probability distribution. Define H : ℕ → ℝ by H(n) := recognition_free_energy(sys, (R.step)^n q₀, X) − recognition_free_energy(sys, π, X). Then H(n) ≥ 0 for all n and H is antitone.
background
A RecognitionSystem fixes a positive recognition temperature T_R. The Gibbs measure π = gibbs_measure(sys, X) is the unique equilibrium distribution that minimizes recognition free energy for the given cost function X. A JDescentOperator on π is a structure whose step map fixes π and satisfies kl_non_increasing: D_KL(step q ‖ π) ≤ D_KL(q ‖ π) for every distribution q (see the structure fields fixes_equilibrium and kl_non_increasing).
proof idea
The tactic proof introduces the local definition of H and refines the conjunction. The left conjunct (nonnegativity) is obtained by applying free_energy_ge_equilibrium to the evolved distribution at step n and discharging the resulting inequality with linarith. The right conjunct (antitone) is obtained by applying free_energy_le_of_le to the free-energy values themselves and again using linarith on the differences.
why it matters
This supplies the single-statement Lyapunov form of the second law and is the direct parent of secondLawCert_inhabited, which inhabits the SecondLawCert certificate. It completes the free-energy monotonicity derivation inside the module that assembles the second law from the J-descent property of the recognition operator. In the broader framework it realizes the monotonicity step that follows from T5 (J-uniqueness) and T7 (eight-tick octave) along the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.