lag_r
plain-language theorem explainer
The equality 45 divided by the product of 8 and 120 equals 3 over 64 holds over the reals and carries a simp attribute for automatic reduction. Workers on Gap45 time-lag identities in the Recognition Science setting cite it when aligning 8-beat octaves with 45-unit cycles. The proof is a direct norm_num evaluation that collapses the arithmetic in one step.
Claim. $45 / (8 * 120) = 3/64$
background
The Gap45 module encodes the gating rule that experience is required exactly when the plan period is not a multiple of 8, implementing the policy that 8-beat alignment disables Gap45 gating. The lemma supplies a normalized real-arithmetic identity used inside lag computations that mix the 8-tick octave with 45-unit periods. The upstream TimeLag result states the same fact verbatim: 'As reals: 45 / (8 * 120) = 3 / 64.'
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to both sides of the equality, reducing the concrete integer arithmetic without invoking any other lemmas.
why it matters
This identity feeds the TimeLag.lag_r declaration and supports simplifications throughout Gap45 beat-alignment proofs. It instantiates the eight-tick octave (T7) by isolating the factor of 8 that appears in period calculations, and the resulting 3/64 ratio enters downstream lag expressions. No open scaffolding remains once the norm_num reduction is accepted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.