  31  | novice | beginner | competent | proficient | expert
  32  deriving DecidableEq, Repr, BEq, Fintype
  33
  34theorem masteryStageCount : Fintype.card MasteryStage = 5 := by decide
  35
  36/-- Optimal study block = φ hours. -/
  37noncomputable def optimalBlockHours : ℝ := phi
  38
  39/-- Block is between 1 and 2 hours. -/
  40theorem optimalBlock_in_range :
  41    (1 : ℝ) < optimalBlockHours ∧ optimalBlockHours < 2 := by
  42  unfold optimalBlockHours
  43  exact ⟨one_lt_phi, by linarith [phi_lt_onePointSixTwo]⟩
  44
  45/-- Recovery ratio = 1/φ (inverse of study block). -/
  46noncomputable def recoveryRatio : ℝ := phi⁻¹
  47
  48theorem recovery_ratio_pos : 0 < recoveryRatio := by
  49  unfold recoveryRatio; exact inv_pos.mpr phi_pos
  50
  51/-- Mastery hours per rung = 45. -/
  52def masteryHoursPerRung : ℕ := 45
  53
  54theorem masteryHours_eq_gap45 : masteryHoursPerRung = 45 := rfl
  55
  56/-- Hours at rung k = 45 × φᵏ (scaling). -/
  57noncomputable def masteryAtRung (k : ℕ) : ℝ := (masteryHoursPerRung : ℝ) * phi ^ k
  58
  59theorem masteryAtRung_pos (k : ℕ) : 0 < masteryAtRung k := by
  60  unfold masteryAtRung masteryHoursPerRung
  61  norm_num
  62  exact pow_pos phi_pos k
  63
  64structure MasteryDesignCert where

papers checked against this theorem

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