recovery_ratio_pos
plain-language theorem explainer
The theorem proves positivity of the recovery ratio in the gap-45 mastery model. Pedagogical designers using Recognition Science would cite it to confirm the break-to-study ratio stays positive when building certified designs. The proof is a one-line term wrapper that unfolds the definition as the reciprocal of phi and invokes the inverse-positivity lemma on the established fact that phi is positive.
Claim. The recovery ratio, defined as the reciprocal of the golden ratio, satisfies $0 < r$ where $r = 1/phi$.
background
The MasteryDesignFromGap45 module sets the recovery ratio to the inverse of the golden ratio as the break-to-study ratio in RS pedagogical design. This follows the module's prediction that optimal study blocks last phi hours with recovery ratio 1/phi, yielding the 10,000-hour rule approximation as gap-45 times phi^5. The definition recoveryRatio := phi^{-1} draws on phi positivity from the imported constants, while the broader setting includes five mastery stages matching configDim D = 5 and the phi-ladder for mastery hours per rung.
proof idea
The proof is a one-line term-mode wrapper. It unfolds recoveryRatio to obtain phi^{-1} and applies inv_pos.mpr directly to phi_pos.
why it matters
The result supplies the recovery_pos field required by masteryDesignCert, which certifies the full set of design parameters including five stages, block range, mastery hours equal to gap-45, and positivity at each rung. It closes the positivity check for the recovery parameter, aligning with the phi self-similar fixed point (T6) and the eight-tick octave structure in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.