masteryStageCount
plain-language theorem explainer
The result asserts that the inductive type of mastery stages in the Recognition Science educational framework has exactly five elements. Pedagogical designers referencing the gap-45 threshold would invoke this cardinality when assembling certification records for study protocols. The proof proceeds by a single decide tactic that computes the cardinality directly from the five constructors of the inductive definition.
Claim. The finite set consisting of the five mastery stages novice, beginner, competent, proficient, and expert has cardinality five: $|S| = 5$ where $S$ denotes that set.
background
The module develops educational design principles from the gap-45 mastery threshold, where 45 hours per rung achieve mastery and optimal study blocks equal phi hours. MasteryStage is defined as the inductive type with constructors novice, beginner, competent, proficient, expert, deriving Fintype among other instances. This cardinality result supplies one of the fields required by the MasteryDesignCert structure that bundles the five-stage count with block-range, recovery-ratio, and mastery-hours properties.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality Fintype.card MasteryStage = 5. Since the inductive type is finite with exactly five constructors, the decision procedure succeeds by exhaustive enumeration.
why it matters
This theorem populates the five_stages field of the masteryDesignCert definition, which certifies the complete set of pedagogical invariants derived from the gap-45 model. It directly implements the module's claim that five canonical mastery stages equal configDim D = 5, aligning with the Recognition Science prediction of discrete stages in educational progression. The result closes the scaffolding for the educational certification object without introducing open hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.