per_session_eq
plain-language theorem explainer
The per-session duration equals exactly 45 divided by 8 hours in the optimal pedagogy schedule. Education researchers calibrating mastery acquisition against the gap-45 threshold would cite this when fixing session lengths to the eight-tick structure. The proof is a one-line term that unfolds the three definitions and reduces the arithmetic via norm_num.
Claim. The per-session duration satisfies $45/8$ hours, where the total per-rung mastery time of 45 hours is distributed over the 8-tick session count.
background
perRungHours is the gap-45 hours required per rung for mastery. sessionCount is the 8-tick session count per rung, fixed at 8. perSessionHours is defined as the rational quotient of perRungHours by sessionCount. The module derives the optimal time distribution within each 45-hour rung as 8-tick spaced sessions, aligning distributed practice with the eight-tick octave. Upstream results supply the concrete values 45 and 8, which this equality combines.
proof idea
The proof is a one-line term that unfolds perSessionHours, perRungHours, and sessionCount, then applies norm_num to simplify the resulting arithmetic expression.
why it matters
This equality is invoked directly in the construction of PedagogyOptimalCert and in the proofs of per_session_in_band, per_session_value, and total_eq_session_times_count. It supplies the concrete per-session length required by the E5 Deepening step that links the gap-45 mastery threshold to the eight-tick session structure (T7 of the forcing chain). Downstream results use it to place the session length inside the interval [5,6] and to recover the total rung time as 8 times the session length.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.