forgetting_decreases
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not address how emotional weight modifies the forgetting rate.
- Does not extend the statement to continuous time or non-integer cycle counts.
- Does not claim strict inequality when n equals m.
- Does not depend on the complexity or consolidation fields of the trace.
formal statement (Lean)
216theorem forgetting_decreases (trace : LedgerMemoryTrace) (n m : ℕ) (t : ℕ)
217 (h : n ≤ m) (hs : trace.strength > 0) (ht : trace.encoding_tick ≤ t) :
218 apply_forgetting trace m t ≤ apply_forgetting trace n t := by
proof body
Tactic-mode proof.
219 unfold apply_forgetting forgetting_rate
220 have h_mcost : 0 ≤ memory_cost trace t := memory_cost_nonneg trace t hs ht
221 have h_rate : 0 ≤ base_decay_rate * memory_cost trace t / breath_cycle :=
222 div_nonneg (mul_nonneg base_decay_rate_pos.le h_mcost) breath_cycle_pos.le
223 apply mul_le_mul_of_nonneg_left _ trace.strength_bounded.1
224 rw [exp_le_exp]
225 have h_nm : (n : ℝ) ≤ (m : ℝ) := by norm_cast
226 have h_window : 0 < (working_memory_window : ℝ) := by norm_num [working_memory_window]
227 nlinarith [mul_nonneg h_rate (le_of_lt h_window)]
228
229/-- Emotional memories forget slower -/