recognition / Education / Education.MasteryDesignFromGap45 / masteryDesignCert

def

`masteryDesignCert`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Education.MasteryDesignFromGap45 on GitHub at line 71.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

depends on

used by

masteryDesignCert IndisputableMonolith.Education.MasteryDesignFromJCost

formal source

  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.