memory_cost
plain-language theorem explainer
memory_cost assembles the retention cost of a LedgerMemoryTrace at a given tick from complexity, elapsed time, and interference terms, each multiplied by an emotional discount. Researchers deriving forgetting rates or equilibrium remember probabilities in Recognition Science thermodynamics cite this definition when quantifying free-energy decay of memory. The definition is an explicit arithmetic combination of four component costs with no external lemmas or tactics.
Claim. For a trace with complexity $c$, strength $s$, emotional weight $w$, encoding tick $t_e$, and ledger balance $b$, the memory cost at tick $t$ equals $(1 - w(1 - 1/φ)) · (c · J(s) + log(1 + (t - t_e)/B) + J(1 + |b|/10))$, where $B = 1024$ is the breath cycle and $J$ is the J-cost function.
background
The MemoryLedger module treats memory as a thermodynamic system in Recognition Science whose retention competes with free-energy decay. The central data structure is LedgerMemoryTrace, which records complexity (positive real), strength and emotional_weight (each in [0,1]), encoding_tick, ledger_balance, and a consolidated flag. breath_cycle supplies the fixed time scale 1024 used for the logarithmic time term. Upstream results include the LedgerMemoryTrace structure definition and the breath_cycle constant.
proof idea
The definition is built by direct let-bindings: time_elapsed subtracts the encoding tick from the current tick, complexity_cost multiplies complexity by Jcost of strength, time_cost applies log to one plus elapsed divided by breath_cycle, interference_cost applies Jcost to one plus absolute balance over ten, emotional_discount subtracts emotional_weight times (1 - 1/φ), and the result multiplies the discount by the sum of the three costs.
why it matters
This definition is invoked by nine downstream results including emotional_reduces_cost (higher emotional weight lowers cost), forgetting_rate (scales the cost by base_decay_rate over breath_cycle), and equilibrium_remember_prob (inserts the cost into a Boltzmann factor). It operationalizes the module claim that memory retention versus free-energy decay is a solvable physics problem and connects to the J-cost and phi-based scaling of the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.