forgetting_decreases

formal source

 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
 243  have h_strength_eq : trace1.strength = trace2.strength := h_same.2.1
 244  -- Lower cost => lower rate => smaller negative exponent => larger exp result
 245  have h_cost_lt : memory_cost trace1 t < memory_cost trace2 t :=
 246    emotional_reduces_cost trace1 trace2 t h_same h_more hs1 hs2 ht1 h_not_perfect