cert
plain-language theorem explainer
The definition cert assembles the complete certificate for optimal pedagogy rate derived from the 45-hour mastery rung and eight-tick structure. Researchers in learning science optimizing distributed practice schedules would reference it to ground claims about session length and spacing. It is assembled as a structure instance that directly references prior equalities and inequalities without additional proof steps.
Claim. The certificate states that per-rung hours equal 45, session count equals 8, per-session hours equal $45/8$, the total time satisfies per-rung hours equals session count times per-session hours, the optimal spacing ratio is positive, and lies strictly between 1 and 2.
background
This module derives the optimal distribution of the 45-hour mastery threshold across sessions using the eight-tick structure. The structure PedagogyOptimalCert collects the key relations: per-rung mastery requires 45 hours, split into 8 sessions, yielding 5.625 hours per session, with total equality holding by construction, and optimal spacing ratio satisfying 0 < ratio < 2. Upstream results establish the per-session length via norm_num simplification and the spacing bounds via one_lt_phi and phi_lt_two.
proof idea
The definition is a structure constructor that supplies rfl for the per-rung and session-count equalities. It invokes per_session_eq for the per-session value, total_eq_session_times_count for the total relation, spacing_ratio_pos for positivity, and the pair spacing_above_one together with spacing_below_two for the interval membership.
why it matters
This certificate completes the derivation of the optimal pedagogy rate in the Education module, bundling results that follow from the eight-tick octave structure and the gap-45 mastery threshold. It directly supports the claim that distributed practice with phi spacing maximizes retention, consistent with the Recognition Science forcing chain at T7. No downstream uses are recorded yet, leaving open its integration into larger learning models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.