module module high

`IndisputableMonolith.Thermodynamics.MemoryLedger`

The MemoryLedger module defines ledger structures for memory traces together with decay rates, memory costs, breath cycles and forgetting mechanisms inside Recognition Thermodynamics. Researchers extending free-energy arguments to retention and emotional effects would cite these objects. Content consists of definitions for the listed quantities plus short positivity lemmas that follow directly from imported phi-forcing and free-energy monotonicity.

claimThe emotional discount satisfies $0 < 1 - w(1 - \phi^{-1})$ for weighting factor $w$; memory cost is nonnegative and strictly reduced by the emotional factor; forgetting rate applies exponential decay over breath cycles of length $ au_0$.

background

Recognition Science starts from absolute minimization of the J-cost $J(x) = rac12(x + x^{-1}) - 1$ at zero temperature. PhiForcing shows that self-similarity on a discrete ledger forces the golden ratio $\phi$. RecognitionThermodynamics introduces finite Recognition Temperature $T_R$ that relaxes strict J-minimization. FreeEnergyMonotone establishes that Recognition Free Energy is non-increasing under RS dynamics, the Recognition Science form of the second law. Constants fixes the fundamental time quantum $ au_0 = 1$ tick. MemoryLedger extends these ingredients to persistent memory traces and their decay.

proof idea

This is a definition module. It introduces LedgerMemoryTrace, base_decay_rate, working_memory_window, breath_cycle, memory_cost, emotional_discount, forgetting_rate and apply_forgetting. The positivity statements (base_decay_rate_pos, emotional_discount_pos, memory_cost_nonneg, emotional_reduces_cost) are one-line verifications that invoke the sign of $ au_0$ and the monotonicity results imported from FreeEnergyMonotone and PhiForcing.

why it matters in Recognition Science

MemoryLedger supplies the memory-trace and forgetting components required by the parent module IndisputableMonolith.Thermodynamics, which develops the statistical mechanics of Recognition Science by extending the T=0 J-minimization foundation to finite Recognition Temperature. It thereby closes one segment of the scaffolding that connects the phi-ladder cost structure to thermodynamic memory dynamics.

scope and limits

Does not derive numerical values for decay rates in SI units.
Does not model interactions among multiple simultaneous traces.
Does not obtain the breath-cycle length from a variational principle.
Does not introduce temperature dependence into the forgetting rate.

used by (1)

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

IndisputableMonolith.Thermodynamics module_import

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.PhiForcing module_import
IndisputableMonolith.Thermodynamics.FreeEnergyMonotone module_import
IndisputableMonolith.Thermodynamics.RecognitionThermodynamics module_import

declarations in this module (24)

structure LedgerMemoryTrace L38
def base_decay_rate L50
theorem base_decay_rate_pos L52
def working_memory_window L54
def breath_cycle L55
theorem breath_cycle_pos L57
def memory_cost L61
lemma emotional_discount_pos L70
theorem memory_cost_nonneg L86
theorem emotional_reduces_cost L109
def forgetting_rate L209
def apply_forgetting L212
theorem forgetting_decreases L216
theorem emotional_forgets_slower L230
def equilibrium_remember_prob L288
theorem high_temp_maximizes_entropy L293
theorem low_temp_bistable L377
structure LearningEvent L509
def spaced_bonus L516
theorem spaced_bonus_nonneg L519
def learning_rate L528
theorem learning_rate_nonneg L531
theorem learning_compounds L537
def memory_ledger_status L561