def
definition
def or abbrev
memory_cost
show as:
view Lean formalization →
formal statement (Lean)
61noncomputable def memory_cost (trace : LedgerMemoryTrace) (current_tick : ℕ) : ℝ :=
proof body
Definition body.
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/φ)) -/