`sessionCount`

definition

show as: view math explainer →

module: IndisputableMonolith.Education.PedagogyOptimalRateFromGap45
domain: Education
line: 56 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Education.PedagogyOptimalRateFromGap45 on GitHub at line 56.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  53def perRungHours : ℕ := 45
  54
  55/-- 8-tick session count per rung. -/
  56def sessionCount : ℕ := 8
  57
  58/-- Per-session length in hours (rational). -/
  59def perSessionHours : ℚ := (perRungHours : ℚ) / sessionCount
  60
  61theorem per_session_eq : perSessionHours = 45 / 8 := by
  62  unfold perSessionHours perRungHours sessionCount; norm_num
  63
  64/-- Per-session ≈ 5.625 hours. -/
  65theorem per_session_value : perSessionHours = 5625 / 1000 := by
  66  rw [per_session_eq]; norm_num
  67
  68/-- Total per-rung = 45 hours = 8 × 5.625. -/
  69theorem total_eq_session_times_count :
  70    (perRungHours : ℚ) = sessionCount * perSessionHours := by
  71  rw [per_session_eq]
  72  unfold sessionCount perRungHours; norm_num
  73
  74/-- Per-session length in [5, 6] hours. -/
  75theorem per_session_in_band : (5 : ℚ) ≤ perSessionHours ∧ perSessionHours ≤ 6 := by
  76  rw [per_session_eq]
  77  refine ⟨?_, ?_⟩ <;> norm_num
  78
  79/-- Optimal spacing ratio between consecutive sessions = φ. -/
  80def optimalSpacingRatio : ℝ := phi
  81
  82theorem spacing_ratio_pos : 0 < optimalSpacingRatio := phi_pos
  83
  84/-- Spacing ratio > 1 (distributed practice beats massed). -/
  85theorem spacing_above_one : 1 < optimalSpacingRatio := one_lt_phi
  86

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.