`LedgerMemoryTrace`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Thermodynamics.MemoryLedger on GitHub at line 38.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

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

papers checked against this theorem

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