working_memory_window

formal source

  51
  52theorem base_decay_rate_pos : 0 < base_decay_rate := div_pos zero_lt_one phi_pos
  53
  54def working_memory_window : ℕ := 8
  55def breath_cycle : ℕ := 1024
  56
  57theorem breath_cycle_pos : 0 < (breath_cycle : ℝ) := by unfold breath_cycle; norm_num
  58
  59/-! ## Memory J-Cost -/
  60
  61noncomputable def memory_cost (trace : LedgerMemoryTrace) (current_tick : ℕ) : ℝ :=
  62  let time_elapsed := (current_tick - trace.encoding_tick : ℝ)
  63  let complexity_cost := trace.complexity * Jcost trace.strength
  64  let time_cost := log (1 + time_elapsed / breath_cycle)
  65  let interference_cost := Jcost (1 + |trace.ledger_balance| / 10)
  66  let emotional_discount := 1 - trace.emotional_weight * (1 - 1/φ)
  67  emotional_discount * (complexity_cost + time_cost + interference_cost)
  68
  69/-- Emotional discount is always positive (0 < 1 - w*(1 - 1/φ)) -/
  70lemma emotional_discount_pos (trace : LedgerMemoryTrace) :
  71    0 < 1 - trace.emotional_weight * (1 - 1/φ) := by
  72  have h1 : 1 < φ := phi_gt_one
  73  have h2 : 0 < φ := phi_pos
  74  have h2' : 0 < 1/φ := div_pos one_pos h2
  75  have h3 : 1/φ < 1 := by rw [div_lt_one h2]; exact h1
  76  have h4 : 0 < 1 - 1/φ := by linarith
  77  have h4' : 1 - 1/φ < 1 := by linarith
  78  have hw := trace.emotional_bounded
  79  have h5 : trace.emotional_weight * (1 - 1/φ) < 1 := by
  80    calc trace.emotional_weight * (1 - 1/φ)
  81        ≤ 1 * (1 - 1/φ) := mul_le_mul_of_nonneg_right hw.2 (le_of_lt h4)
  82      _ = 1 - 1/φ := one_mul _
  83      _ < 1 := h4'
  84  linarith