emotional_reduces_cost
plain-language theorem explainer
Emotional memories incur strictly lower retention costs than neutral ones when all other trace parameters match. Researchers modeling memory decay in Recognition Science would cite this to justify slower forgetting for emotionally weighted traces. The proof proceeds by showing that the base cost is identical while the emotional discount factor is strictly smaller for the higher-weight trace, then applying positivity of the base cost and monotonicity of multiplication.
Claim. Let $T_1$ and $T_2$ be memory traces with identical complexity, strength, encoding tick, and ledger balance, but with emotional weight $w_1 > w_2$. For any time $t$ at or after the encoding tick of $T_1$, and assuming the trace is imperfect (strength less than 1, or $t$ exceeds the encoding tick, or nonzero ledger balance), the memory cost of $T_1$ at $t$ is strictly less than the memory cost of $T_2$ at $t$.
background
In the Memory Ledger module, memory retention is modeled as a thermodynamic process where the cost of maintaining a trace is given by memory_cost, which multiplies a base cost (involving J-cost of strength and ledger balance, plus a logarithmic term for time elapsed) by an emotional discount factor of the form $1 - w (1 - 1/φ)$, where $w$ is the emotional_weight and $φ$ is the golden ratio. The LedgerMemoryTrace structure records complexity (positive real), emotional_weight (bounded in [0,1]), strength (bounded in [0,1]), encoding_tick, and ledger_balance.
proof idea
The proof unfolds memory_cost and establishes equality of the undiscounted base terms via the h_same hypothesis. It shows the discount for trace1 is strictly smaller than for trace2 by mul_lt_mul_of_pos_right on the emotional weights and the positive coefficient (1-1/φ), using phi_gt_one and phi_pos. Positivity of discounts follows from emotional_discount_pos. Base cost positivity is obtained by case analysis on h_not_perfect, invoking Jcost_pos_of_ne_one when strength <1, log_pos when t exceeds the tick, and a similar positivity argument for nonzero balance. The final inequality is obtained by mul_lt_mul_of_pos_right on the smaller discount and positive base.
why it matters
This result directly supports the downstream theorem emotional_forgets_slower, which uses it to establish slower forgetting rates, and appears in the memory_ledger_status summary confirming all thermodynamic memory theorems are proven. It fills the step linking emotional weighting to reduced free-energy decay costs, relying on the phi-based discounting and J-cost positivity that appear throughout the Recognition Science forcing chain and cost definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.