optimalBlock_in_range

formal source

  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
  65  five_stages : Fintype.card MasteryStage = 5
  66  block_range : (1 : ℝ) < optimalBlockHours ∧ optimalBlockHours < 2
  67  recovery_pos : 0 < recoveryRatio
  68  mastery_hours : masteryHoursPerRung = 45
  69  mastery_pos : ∀ k, 0 < masteryAtRung k
  70