learning_compounds

formal source

 534  · apply mul_nonneg (rpow_pos_of_pos phi_pos _).le event.attention_bounded.1
 535  · linarith [spaced_bonus_nonneg event]
 536
 537theorem learning_compounds (e1 e2 : LearningEvent)
 538    (h_same : e1.experience = e2.experience)
 539    (h_more : e1.repetitions > e2.repetitions)
 540    (h_attn : e1.attention = e2.attention)
 541    (h_space : e1.spacing = e2.spacing)
 542    (hs1 : e1.experience.strength > 0) (_hs2 : e2.experience.strength > 0) :
 543    let dr1 := -learning_rate e1 * memory_cost e1.experience e1.experience.encoding_tick
 544    let dr2 := -learning_rate e2 * memory_cost e2.experience e2.experience.encoding_tick
 545    dr1 ≥ dr2 := by
 546  intro dr1 dr2
 547  have h_pow_le : φ ^ (-(e1.repetitions : ℝ)) ≤ φ ^ (-(e2.repetitions : ℝ)) := by
 548    apply rpow_le_rpow_of_exponent_le (le_of_lt phi_gt_one)
 549    simp only [neg_le_neg_iff, Nat.cast_le]; exact Nat.le_of_lt h_more
 550  have h_bonus : spaced_bonus e1 = spaced_bonus e2 := by unfold spaced_bonus; rw [h_space]
 551  have h_lr_le : learning_rate e1 ≤ learning_rate e2 := by
 552    unfold learning_rate; rw [h_attn, h_bonus]
 553    apply mul_le_mul_of_nonneg_right _ (by linarith [spaced_bonus_nonneg e2])
 554    apply mul_le_mul_of_nonneg_right h_pow_le e2.attention_bounded.1
 555  have h_cost_same : memory_cost e1.experience e1.experience.encoding_tick =
 556                     memory_cost e2.experience e2.experience.encoding_tick := by rw [h_same]
 557  have h_cost_nonneg : 0 ≤ memory_cost e1.experience e1.experience.encoding_tick :=
 558    memory_cost_nonneg _ _ hs1 (le_refl _)
 559  simp only [dr1, dr2]; rw [h_cost_same]; nlinarith
 560
 561def memory_ledger_status : List (String × String) :=
 562  [ ("memory_cost_nonneg", "PROVEN")
 563  , ("emotional_reduces_cost", "PROVEN")
 564  , ("forgetting_decreases", "PROVEN")
 565  , ("emotional_forgets_slower", "PROVEN")
 566  , ("high_temp_maximizes_entropy", "PROVEN")
 567  , ("low_temp_bistable", "PROVEN")