masteryAtRung_pos
plain-language theorem explainer
The theorem shows that mastery hours at rung k equal 45 times phi to the k and are therefore strictly positive for every natural number k. Educational designers working from the gap-45 model cite it to guarantee that every mastery threshold on the phi-ladder remains positive. The proof is a one-line term that unfolds the two definitions, reduces the constant 45 by norm_num, and applies the standard positivity lemma for powers of phi.
Claim. For every natural number $k$, the mastery hours at rung $k$ satisfy $45 · φ^k > 0$, where mastery hours at rung $k$ are defined by scaling the base 45-hour rung by the factor $φ^k$.
background
The module Education.MasteryDesignFromGap45 implements the RS prediction that mastery requires 45 hours per rung on the phi-ladder (gap-45 = body-plan ceiling). The auxiliary definition masteryHoursPerRung fixes the base at 45; masteryAtRung then scales it by phi^k. The module also records optimal block size phi hours, recovery ratio 1/phi, and five canonical stages matching configDim D = 5. Upstream, the positivity of phi itself is supplied by the Constants module.
proof idea
The term proof unfolds masteryAtRung and masteryHoursPerRung, applies norm_num to obtain the concrete expression 45 * phi^k, and finishes with the exact application of pow_pos phi_pos k.
why it matters
masteryAtRung_pos is one of the five fields required to construct the MasteryDesignCert record. That certificate packages the gap-45 predictions (five stages, block range, recovery positivity, mastery hours, and mastery positivity) into a single verified object. The result therefore closes the last positivity obligation in the educational-design chain that begins from the phi-ladder and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.