pith. machine review for the scientific record. sign in
theorem proved tactic proof

memory_cost_nonneg

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  86theorem memory_cost_nonneg (trace : LedgerMemoryTrace) (t : ℕ)
  87    (hs : trace.strength > 0) (ht : trace.encoding_tick ≤ t) :
  88    0 ≤ memory_cost trace t := by

proof body

Tactic-mode proof.

  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
  92  -- Sum of nonnegatives is nonnegative
  93  have h1 : 0 ≤ trace.complexity * Jcost trace.strength :=
  94    mul_nonneg trace.complexity_pos.le (Jcost_nonneg hs)
  95  have h2 : 0 ≤ log (1 + (↑t - ↑trace.encoding_tick) / ↑breath_cycle) := by
  96    apply log_nonneg
  97    have hd : 0 ≤ (↑t - ↑trace.encoding_tick : ℝ) := by simp [sub_nonneg, Nat.cast_le, ht]
  98    linarith [div_nonneg hd (le_of_lt breath_cycle_pos)]
  99  have h3 : 0 ≤ Jcost (1 + (↑|trace.ledger_balance| : ℝ) / 10) := by
 100    apply Jcost_nonneg
 101    -- |trace.ledger_balance| ≥ 0 as an integer, so its cast to ℝ is also ≥ 0
 102    have h_abs_nonneg : (0 : ℤ) ≤ |trace.ledger_balance| := abs_nonneg _
 103    have h_cast_nonneg : (0 : ℝ) ≤ ↑|trace.ledger_balance| := by norm_cast
 104    linarith [div_nonneg h_cast_nonneg (by norm_num : (0 : ℝ) ≤ 10)]
 105  -- Sum of nonnegative terms is nonnegative
 106  exact add_nonneg (add_nonneg h1 h2) h3
 107
 108/-- Emotional memories have lower cost -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (23)

Lean names referenced from this declaration's body.