spaced_bonus_nonneg
plain-language theorem explainer
The theorem shows that spaced_bonus is nonnegative for every LearningEvent in the memory ledger. Physicists modeling retention as a thermodynamic process cite it to guarantee nonnegative learning rates. The proof unfolds the definition then chains div_nonneg with two applications of log_nonneg, using norm_cast, omega, and linarith to confirm the argument of the first logarithm is nonnegative.
Claim. $0 ≤ log(1 + spacing(e)/8) / log φ$ for every learning event $e$, where spacing($e$) is the repetition interval in the event structure, the working-memory window equals 8, and $φ$ denotes the golden ratio.
background
The MemoryLedger module treats memory retention as a thermodynamic balance between free-energy decay and recognition cost. A LearningEvent packages a LedgerMemoryTrace together with bounded attention, repetition count, and spacing (a natural number). The spaced_bonus function is defined as log(1 + spacing / working_memory_window) / log φ with working_memory_window fixed at 8. Upstream, phi_ge_one supplies 1 ≤ φ, which is required for the logarithm in the denominator to be nonnegative.
proof idea
Unfold spaced_bonus, then apply div_nonneg. The first subgoal uses log_nonneg after establishing 0 ≤ spacing / 8 via norm_cast, omega, and linarith against the positive window constant. The second subgoal invokes log_nonneg directly on phi_ge_one.
why it matters
spaced_bonus_nonneg is invoked inside learning_rate_nonneg and learning_compounds, both of which appear in the module's list of fully proven thermodynamic memory theorems. It supplies the nonnegativity step needed to close the learning-rate claim and thereby supports the broader Recognition Science treatment of memory as a solvable physics problem governed by the phi-ladder and J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.