spacing_above_one
plain-language theorem explainer
The theorem establishes that the optimal spacing ratio between consecutive learning sessions exceeds 1, confirming distributed practice outperforms massed practice in the Recognition Science pedagogy model. Education researchers modeling mastery thresholds would cite this result when deriving session distributions from the 45-hour per-rung gap. The proof is a direct one-line application of the known inequality for the golden ratio.
Claim. The optimal spacing ratio between consecutive sessions satisfies $1 < phi$, where $phi$ is the golden ratio.
background
In the Recognition Science framework the per-rung mastery threshold is fixed at 45 hours. Within each rung the optimal time distribution follows an 8-tick octave, producing eight sessions whose inter-session spacing ratio is defined as the golden ratio phi. The module therefore derives per-session length 45/8 hours and asserts that geometric spacing with ratio phi maximises retention probability per learner.
proof idea
The proof is a one-line wrapper that applies the lemma one_lt_phi to the definition optimalSpacingRatio := phi.
why it matters
This result supplies the spacing_pos field inside the PedagogyOptimalCert definition, completing the derivation of optimal pedagogy rate from the gap-45 threshold. It instantiates the eight-tick octave and the self-similar fixed point phi inside the education domain. The module falsifier remains any prospective trial showing optimal ratio outside the phi band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.