second_law_one_statement
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.
claimLet 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 in Recognition Science
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.
scope and limits
- Does not establish the entropy form of the second law without the extra hypothesis that expected cost is conserved.
- Does not apply to continuous-time flows or infinite configuration spaces.
- Does not quantify the convergence rate to equilibrium.
- Does not assume any concrete Markov kernel beyond the abstract J-descent axioms.
formal statement (Lean)
300theorem second_law_one_statement (sys : RecognitionSystem) (X : Ω → ℝ)
301 (R : JDescentOperator (gibbsPD sys X)) (q₀ : ProbabilityDistribution Ω) :
302 let H : ℕ → ℝ := fun n =>
proof body
Tactic-mode proof.
303 recognition_free_energy sys (R.evolve n q₀).p X -
304 recognition_free_energy sys (gibbs_measure sys X) X
305 (∀ n : ℕ, 0 ≤ H n) ∧ Antitone H := by
306 intro H
307 refine ⟨?_, ?_⟩
308 · intro n
309 show 0 ≤ recognition_free_energy sys (R.evolve n q₀).p X -
310 recognition_free_energy sys (gibbs_measure sys X) X
311 have := free_energy_ge_equilibrium sys X R q₀ n
312 linarith
313 · intro n m hnm
314 show recognition_free_energy sys (R.evolve m q₀).p X -
315 recognition_free_energy sys (gibbs_measure sys X) X ≤
316 recognition_free_energy sys (R.evolve n q₀).p X -
317 recognition_free_energy sys (gibbs_measure sys X) X
318 have hF :
319 recognition_free_energy sys (R.evolve m q₀).p X ≤
320 recognition_free_energy sys (R.evolve n q₀).p X :=
321 free_energy_le_of_le sys X R q₀ hnm
322 linarith
323
324/-! ## §7. The Clausius / entropy form -/
325
326/-- **THE SECOND LAW — CLAUSIUS / ENTROPY FORM.**
327
328 If the expected cost `⟨X⟩` is conserved along the J-descent evolution
329 (i.e. the system is energetically isolated), then the recognition entropy
330 `S_R(qₙ) = −Σ qₙ(ω) log qₙ(ω)` is monotone non-decreasing in `n`.
331
332 This is the classical statement `ΔS ≥ 0` for an isolated system,
333 derived from the free-energy form `F = ⟨X⟩ − T_R · S_R`. -/