LearningEvent
plain-language theorem explainer
The LearningEvent structure models a learning occurrence in the thermodynamic memory ledger by bundling a LedgerMemoryTrace experience with bounded attention in [0,1], repetition count, and spacing. Researchers formalizing retention under Recognition Science cite it to parameterize how events update ledger strength and decay rates. It is introduced as a plain structure definition with no computational body or lemmas.
Claim. A learning event consists of a memory trace $e$, attention value $a$ satisfying $0leq a leq 1$, repetition count $r in mathbb{N}$, and spacing interval $s in mathbb{N}$.
background
The MemoryLedger module treats memory retention as a thermodynamic competition between free-energy decay and recognition strength, per Recognition Science. LedgerMemoryTrace records an experience via positive complexity, emotional weight in [0,1], encoding tick, strength in [0,1], and consolidation flag. LearningEvent extends this record with attention, repetitions, and spacing to quantify incremental updates.
proof idea
This is a structure definition that introduces the LearningEvent record type with its five fields and the single boundedness constraint on attention. No lemmas or tactics are invoked; the declaration serves directly as the input type for downstream definitions such as learning_rate and spaced_bonus.
why it matters
LearningEvent supplies the data type for the module's results on learning rates and compounding, including learning_rate_nonneg and spaced_bonus_nonneg. It operationalizes the thermodynamic memory model by encoding attention and spacing effects that modulate decay, consistent with phi-based costs and free-energy monotonicity in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.