LedgerMemoryTrace

formal source

  35
  36/-! ## Memory Trace Structure -/
  37
  38structure LedgerMemoryTrace where
  39  id : ℕ
  40  complexity : ℝ
  41  complexity_pos : 0 < complexity
  42  emotional_weight : ℝ
  43  emotional_bounded : 0 ≤ emotional_weight ∧ emotional_weight ≤ 1
  44  encoding_tick : ℕ
  45  strength : ℝ
  46  strength_bounded : 0 ≤ strength ∧ strength ≤ 1
  47  consolidated : Bool
  48  ledger_balance : ℤ
  49
  50noncomputable def base_decay_rate : ℝ := 1 / φ
  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