memory_ledger_status
plain-language theorem explainer
This definition supplies a static list of proof statuses for the eight theorems that model memory as a thermodynamic ledger. A physicist examining the Recognition Science treatment of learning and forgetting would reference it to confirm the absence of open sorries in the submodule. The construction is a direct enumeration of theorem names with the label PROVEN.
Claim. The memory ledger status is the list of pairs associating each property with its verification status: non-negativity of memory cost with PROVEN, emotional weight reduces cost with PROVEN, forgetting decreases with time with PROVEN, emotional traces forget slower with PROVEN, high temperature maximizes entropy with PROVEN, low temperature bistability with PROVEN, non-negativity of learning rate with PROVEN, and learning compounds with PROVEN.
background
The module treats memory traces as objects carrying complexity, strength, encoding tick, ledger balance, and emotional weight. Memory cost quantifies free-energy expenditure while emotional weight acts as a discount factor. Upstream results supply evaluation maps for counted-once resource expressions and scalar fields, plus the individual theorems establishing monotonicity and sign properties of these quantities.
proof idea
The definition constructs the list by direct enumeration of eight string pairs. No lemmas are applied and no tactics are used; the body is a literal list of theorem names paired with the string PROVEN.
why it matters
The definition records completion of the memory ledger formalization inside the thermodynamics domain. It confirms that all theorems on emotional effects, forgetting rates, temperature dependence of entropy, and learning dynamics are established, aligning with the module claim that memory reduces to retention versus free-energy decay. No further scaffolding remains in this submodule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.