`memory_ledger_status`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Thermodynamics.MemoryLedger on GitHub at line 561.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 558    memory_cost_nonneg _ _ hs1 (le_refl _)
 559  simp only [dr1, dr2]; rw [h_cost_same]; nlinarith
 560
 561def memory_ledger_status : List (String × String) :=
 562  [ ("memory_cost_nonneg", "PROVEN")
 563  , ("emotional_reduces_cost", "PROVEN")
 564  , ("forgetting_decreases", "PROVEN")
 565  , ("emotional_forgets_slower", "PROVEN")
 566  , ("high_temp_maximizes_entropy", "PROVEN")
 567  , ("low_temp_bistable", "PROVEN")
 568  , ("learning_rate_nonneg", "PROVEN")
 569  , ("learning_compounds", "PROVEN")
 570  ]
 571
 572#eval memory_ledger_status
 573
 574end MemoryLedger
 575end Thermodynamics
 576end IndisputableMonolith

papers checked against this theorem

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