MasteryDesignCert
plain-language theorem explainer
The MasteryDesignCert structure anchors educational mastery designs to a CanonicalCert that encodes J-cost properties. Curriculum theorists and educational modelers cite it when calibrating observed practice time against mastery time via the ratio r. The definition is a one-field structure that directly reuses the six-clause CanonicalCert to enforce zero recognition cost at perfect calibration.
Claim. A mastery design certificate consists of a base Canonical certificate satisfying $J(1)=0$, $J(x)=J(1/x)$ for $x≠0$, $J(φ)>0$ with $0.11<J(φ)<0.13$, and $J(1/φ^2)>0$.
background
In Recognition Science the J-cost function satisfies the Recognition Composition Law and vanishes at unity with inversion symmetry. The upstream CanonicalCert supplies the six properties that locate the canonical band around φ and guarantee positive cost away from 1. This E5 module compounds the J-cost approach with the 45-hour-per-rung threshold from MasteryDesignFromGap45, defining per-curriculum-unit cost on the observed-to-mastery time ratio.
proof idea
The structure is introduced directly as a single-field wrapper whose only component is a CanonicalCert. No tactics or lemmas are applied; the definition simply imports the upstream CanonicalCert to supply the required J-band properties.
why it matters
This certificate supplies the J-cost anchor that the downstream masteryDesignCert definitions in both this module and MasteryDesignFromGap45 instantiate. It fills the E5 educational-design step by gating effective versus ineffective curricula through the canonical band, linking directly to the J-function and φ-band landmarks of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.