forgetting_decreases
plain-language theorem explainer
The theorem establishes monotonic decrease of remaining memory strength under repeated forgetting cycles for traces with positive strength. Researchers modeling retention in recognition-based thermodynamic systems would cite it when bounding decay over discrete breath cycles. The proof unfolds the exponential form of the forgetting application, invokes nonnegativity lemmas for the decay rate, reduces via multiplication monotonicity and exp_le_exp, then closes the inequality with nlinarith.
Claim. Let $s > 0$ be the strength of a memory trace encoded at or before time $t$. For natural numbers $n ≤ m$, the remaining strength after $m$ forgetting cycles is at most the remaining strength after $n$ cycles: $s · exp(−r · m · w) ≤ s · exp(−r · n · w)$, where $r$ is the forgetting rate at $t$ and $w$ is the working-memory window.
background
The module treats memory as a thermodynamic system in which retention competes with free-energy decay governed by Recognition Science constants. A LedgerMemoryTrace records id, complexity, emotional weight (in [0,1]), encoding tick, strength (in [0,1]), and consolidation flag. The forgetting application is defined as initial strength times exp(−rate · cycles · working_memory_window), with rate equal to base_decay_rate (1/φ) scaled by memory cost and divided by breath_cycle (1024). This result rests on the positivity theorems base_decay_rate_pos and breath_cycle_pos together with the nonnegativity of memory_cost.
proof idea
The proof unfolds apply_forgetting and forgetting_rate to expose the exponential. It obtains nonnegativity of memory_cost via memory_cost_nonneg and of the composite rate via mul_nonneg and div_nonneg using base_decay_rate_pos and breath_cycle_pos. It then applies mul_le_mul_of_nonneg_left, rewrites the inequality to exp_le_exp, casts the cycle comparison to reals, confirms the window is positive, and finishes with nlinarith on the nonnegativity of rate times window.
why it matters
The declaration appears in the memory_ledger_status summary as one of the fully proven thermodynamic memory results, confirming that the entire suite (memory_cost_nonneg through learning_compounds) carries no sorries. It supplies the monotonicity step needed for decay bounds in the memory ledger model and aligns with the phi-based decay rate and 1024-tick breath cycle that descend from the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.