equilibrium_remember_prob

formal source

 285
 286/-! ## Thermodynamic Limits -/
 287
 288noncomputable def equilibrium_remember_prob (sys : RecognitionSystem) (trace : LedgerMemoryTrace) (t : ℕ) : ℝ :=
 289  let J := memory_cost trace t
 290  exp (-J / sys.TR) / (exp (-J / sys.TR) + 1)
 291
 292/-- At high temperature, p → 0.5 -/
 293theorem high_temp_maximizes_entropy (trace : LedgerMemoryTrace) (t : ℕ) :
 294    ∀ (ε : ℝ), ε > 0 → ∃ T₀ > 0, ∀ sys : RecognitionSystem, sys.TR > T₀ →
 295      |equilibrium_remember_prob sys trace t - 0.5| < ε := by
 296  intro ε hε
 297  -- Let J = memory_cost trace t (some fixed real number)
 298  set J := memory_cost trace t with hJ_def
 299  -- Choose T₀ large enough that -J/T is small
 300  -- We need |exp(-J/T) - 1| < 2ε to ensure |p - 0.5| < ε
 301  -- Using the bound: |exp(x) - 1| ≤ |x| * exp(|x|) for small |x|
 302  -- For T > |J|/(ε), we have |J/T| < ε, giving roughly |exp(-J/T) - 1| < ε*e^ε < 2ε
 303  --
 304  -- Simpler approach: use that |p - 0.5| = |e-1|/(2(e+1)) ≤ |e-1|/2
 305  -- and |exp(x) - 1| → 0 as x → 0.
 306  --
 307  -- Take T₀ = max(1, |J|/ε + |J| + 1) to ensure |-J/T| < ε and well-behaved bounds
 308  use max 1 ((|J| + 1) * (1/ε + 1))
 309  constructor
 310  · apply lt_max_of_lt_left; norm_num
 311  · intro sys hT
 312    have hT_pos : 0 < sys.TR := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) (le_max_left _ _) |>.trans hT
 313    unfold equilibrium_remember_prob; simp only
 314    -- Let e = exp(-J/sys.TR)
 315    set e := exp (-J / sys.TR) with he_def
 316    have he_pos : 0 < e := exp_pos _
 317    have h_denom_pos : 0 < e + 1 := by linarith
 318    -- The key identity: p - 0.5 = (e - 1) / (2(e+1))