memory_cost_nonneg
plain-language theorem explainer
Memory cost for a LedgerMemoryTrace with positive strength is nonnegative at any time after encoding. Thermodynamic models of memory retention in Recognition Science cite this to keep free-energy expenditures physically valid. The proof unfolds the cost definition, factors out the emotional discount, and sums three nonnegative terms obtained from Jcost nonnegativity, log nonnegativity, and arithmetic inequalities.
Claim. Let trace be a LedgerMemoryTrace with strength $>0$ and encoding_tick $leq t$. Then $0 leq$ memory_cost(trace, $t$), where memory_cost is the product of the emotional discount factor and the sum of complexity times J-cost of strength, the logarithm of one plus elapsed ticks over breath cycle, and J-cost of one plus absolute ledger balance over ten.
background
The module treats memory as a thermodynamic system in which retention competes with free-energy decay under Recognition Science rules. LedgerMemoryTrace records complexity (positive real), emotional_weight (in [0,1]), encoding_tick, strength (in (0,1]), ledger_balance, and related fields. Jcost is the Recognition cost function shown nonnegative for positive arguments by the upstream lemma Jcost_nonneg, which rewrites it as a square over a positive denominator and invokes positivity.
proof idea
The tactic proof unfolds memory_cost then applies mul_nonneg using emotional_discount_pos. It builds three auxiliary facts: h1 by mul_nonneg of complexity_pos.le and Jcost_nonneg hs; h2 by log_nonneg after sub_nonneg and div_nonneg establish the argument is at least one; h3 by Jcost_nonneg on the scaled absolute balance. The proof closes with add_nonneg applied twice to the three facts.
why it matters
The result feeds forgetting_decreases (which invokes it to obtain a nonnegative decay rate) and learning_compounds, and appears in the module status list. It supplies the nonnegativity anchor required for the thermodynamic memory ledger, ensuring all derived rates remain consistent with the nonnegative J-costs that originate in the phi-forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.