`forgetting_rate`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Thermodynamics.MemoryLedger on GitHub at line 209.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 206
 207/-! ## Forgetting Dynamics -/
 208
 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) :

papers checked against this theorem

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