`apply_forgetting`

definition

show as: view math explainer →

module: IndisputableMonolith.Thermodynamics.MemoryLedger
domain: Thermodynamics
line: 212 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Thermodynamics.MemoryLedger on GitHub at line 212.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 209noncomputable def forgetting_rate (trace : LedgerMemoryTrace) (t : ℕ) : ℝ :=
 210  base_decay_rate * memory_cost trace t / breath_cycle
 211
 212noncomputable def apply_forgetting (trace : LedgerMemoryTrace) (n_cycles : ℕ) (current_tick : ℕ) : ℝ :=
 213  let rate := forgetting_rate trace current_tick
 214  trace.strength * exp (-rate * n_cycles * working_memory_window)
 215
 216theorem forgetting_decreases (trace : LedgerMemoryTrace) (n m : ℕ) (t : ℕ)
 217    (h : n ≤ m) (hs : trace.strength > 0) (ht : trace.encoding_tick ≤ t) :
 218    apply_forgetting trace m t ≤ apply_forgetting trace n t := by
 219  unfold apply_forgetting forgetting_rate
 220  have h_mcost : 0 ≤ memory_cost trace t := memory_cost_nonneg trace t hs ht
 221  have h_rate : 0 ≤ base_decay_rate * memory_cost trace t / breath_cycle :=
 222    div_nonneg (mul_nonneg base_decay_rate_pos.le h_mcost) breath_cycle_pos.le
 223  apply mul_le_mul_of_nonneg_left _ trace.strength_bounded.1
 224  rw [exp_le_exp]
 225  have h_nm : (n : ℝ) ≤ (m : ℝ) := by norm_cast
 226  have h_window : 0 < (working_memory_window : ℝ) := by norm_num [working_memory_window]
 227  nlinarith [mul_nonneg h_rate (le_of_lt h_window)]
 228
 229/-- Emotional memories forget slower -/
 230theorem emotional_forgets_slower (trace1 trace2 : LedgerMemoryTrace) (n t : ℕ)
 231    (h_same : trace1.complexity = trace2.complexity ∧
 232              trace1.strength = trace2.strength ∧
 233              trace1.encoding_tick = trace2.encoding_tick ∧
 234              trace1.ledger_balance = trace2.ledger_balance)
 235    (h_more : trace1.emotional_weight > trace2.emotional_weight)
 236    (hs1 : trace1.strength > 0) (hs2 : trace2.strength > 0)
 237    (ht1 : trace1.encoding_tick ≤ t) (ht2 : trace2.encoding_tick ≤ t)
 238    (h_not_perfect : trace1.strength < 1 ∨ t > trace1.encoding_tick ∨ trace1.ledger_balance ≠ 0)
 239    (hn : n > 0) :
 240    apply_forgetting trace1 n t > apply_forgetting trace2 n t := by
 241  unfold apply_forgetting forgetting_rate
 242  -- trace1.strength = trace2.strength by h_same

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.