masteryDesignCert
plain-language theorem explainer
The definition constructs a MasteryDesignCert record that packages the gap-45 educational parameters in Recognition Science. Curriculum designers and learning theorists would cite it to fix study-block length at phi hours and mastery at 45 hours per rung. It is assembled by directly supplying five lemmas as the structure fields.
Claim. A MasteryDesignCert asserts that the number of mastery stages is 5, the optimal study block satisfies $1 < phi < 2$ hours, the recovery ratio is positive, mastery requires exactly 45 hours per rung, and mastery time is strictly positive at every rung level $k$.
background
Recognition Science fixes masteryHoursPerRung at 45 hours via the gap-45 body-plan ceiling. OptimalBlockHours is defined as phi, placing the block between 1 and 2 hours, while recoveryRatio is the reciprocal 1/phi. MasteryAtRung k scales as 45 times phi to the power k, remaining positive for all natural k. The module sets five canonical stages (novice through expert) equal to configDim D = 5, consistent with the phi-ladder conventions imported from Constants.
proof idea
The definition is a direct structure constructor that populates each field of MasteryDesignCert from a dedicated lemma: five_stages from masteryStageCount, block_range from optimalBlock_in_range, recovery_pos from recovery_ratio_pos, mastery_hours from masteryHours_eq_gap45, and mastery_pos from masteryAtRung_pos.
why it matters
This certificate is consumed by the parallel masteryDesignCert in MasteryDesignFromJCost. It realizes the E5 prediction that five stages, phi-hour blocks, and 45-hour rungs follow from the gap-45 threshold, linking the phi fixed point (T6) and configDim D = 5 to pedagogical constants. The definition closes the educational interface without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.