`MasteryDesignCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Education.MasteryDesignFromGap45
domain: Education
line: 64 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Education.MasteryDesignFromGap45 on GitHub at line 64.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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
  71noncomputable def masteryDesignCert : MasteryDesignCert where
  72  five_stages := masteryStageCount
  73  block_range := optimalBlock_in_range
  74  recovery_pos := recovery_ratio_pos
  75  mastery_hours := masteryHours_eq_gap45
  76  mastery_pos := masteryAtRung_pos
  77
  78end IndisputableMonolith.Education.MasteryDesignFromGap45

papers checked against this theorem

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