memory_cost

formal source

  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
  85
  86theorem memory_cost_nonneg (trace : LedgerMemoryTrace) (t : ℕ)
  87    (hs : trace.strength > 0) (ht : trace.encoding_tick ≤ t) :
  88    0 ≤ memory_cost trace t := by
  89  unfold memory_cost; dsimp only
  90  apply mul_nonneg (le_of_lt (emotional_discount_pos trace))
  91  -- Each term is nonnegative: complexity*Jcost ≥ 0, log(1+...) ≥ 0, Jcost(...) ≥ 0