structure
definition
def or abbrev
SecondLawCert
show as:
view Lean formalization →
formal statement (Lean)
374structure SecondLawCert (sys : RecognitionSystem) (X : Ω → ℝ) where
375 /-- Gibbs inequality: the KL divergence to Gibbs is non-negative. -/
376 gibbs_inequality :
377 ∀ q : ProbabilityDistribution Ω,
378 0 ≤ kl_divergence q.p (gibbs_measure sys X)
379 /-- Variational principle: Gibbs minimizes the free energy. -/
380 gibbs_minimizes :
381 ∀ q : ProbabilityDistribution Ω,
382 recognition_free_energy sys (gibbs_measure sys X) X ≤
383 recognition_free_energy sys q.p X
384 /-- Free-energy / KL identity: `F(q) − F(π) = T_R · D_KL(q ‖ π)`. -/
385 fe_kl_identity :
386 ∀ q : ProbabilityDistribution Ω,
387 recognition_free_energy sys q.p X -
388 recognition_free_energy sys (gibbs_measure sys X) X =
389 sys.TR * kl_divergence q.p (gibbs_measure sys X)
390 /-- KL is antitone along any J-descent evolution. -/
391 kl_monotone :
392 ∀ (R : JDescentOperator (gibbsPD sys X)) (q₀ : ProbabilityDistribution Ω),
393 Antitone (fun n : ℕ =>
394 kl_divergence (R.evolve n q₀).p (gibbs_measure sys X))
395 /-- Free energy is antitone along any J-descent evolution. -/
396 free_energy_monotone :
397 ∀ (R : JDescentOperator (gibbsPD sys X)) (q₀ : ProbabilityDistribution Ω),
398 Antitone (fun n : ℕ => recognition_free_energy sys (R.evolve n q₀).p X)
399 /-- Recognition entropy is monotone non-decreasing under conserved energy. -/
400 entropy_monotone_under_conservation :
401 ∀ (R : JDescentOperator (gibbsPD sys X)) (q₀ : ProbabilityDistribution Ω),
402 (∀ n : ℕ, expected_cost (R.evolve n q₀).p X = expected_cost q₀.p X) →
403 Monotone (fun n : ℕ => recognition_entropy (R.evolve n q₀).p)
404
405/-- The master certificate is inhabited. -/