apply_forgetting
plain-language theorem explainer
This definition computes the remaining strength of a memory trace after a given number of forgetting cycles via exponential decay driven by the instantaneous forgetting rate. Researchers modeling thermodynamic retention and free-energy costs in Recognition Science would cite it when deriving monotonicity or emotional modulation results. It is a direct algebraic definition that multiplies initial strength by exp of the negative product of rate, cycle count, and the fixed window of eight.
Claim. For a memory trace $M$ with strength $s(M)$, the strength after $n$ forgetting cycles at tick $t$ equals $s(M)·exp(-r(M,t)·n·8)$, where $r(M,t)$ is the forgetting rate of $M$ at tick $t$.
background
The Memory Ledger module treats memory traces as thermodynamic objects whose retention competes with free-energy decay. A LedgerMemoryTrace carries complexity, emotional weight in [0,1], encoding tick, and bounded strength in [0,1]. The forgetting rate is defined as base decay rate times memory cost at the current tick, divided by breath cycle length. The working memory window is the constant 8.
proof idea
The definition first evaluates the forgetting rate at the supplied trace and tick, then multiplies the trace strength by the exponential of minus that rate times the cycle count times the working memory window of 8. It is a direct one-line wrapper around the forgetting rate and exponential functions with no additional lemmas.
why it matters
This definition supplies the explicit forgetting operator used by the theorems emotional_forgets_slower and forgetting_decreases. It closes the operational gap between the rate definition and the monotonicity statements that establish slower decay for higher emotional weight. The construction aligns with the module's thermodynamic framing of memory as retention versus free-energy decay.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.