lag_q
plain-language theorem explainer
The rational equality 45 divided by 8 times 120 equals 3 over 64 is recorded as a simp lemma. Gap45 calculations in Recognition Science cite it to simplify lag expressions during beat or time-lag reductions. The proof is a direct one-line application of norm_num that normalizes the fractions.
Claim. $45 / (8 * 120) = 3 / 64$ holds in the rationals.
background
Gap45.TimeLag supplies arithmetic facts for lag computations inside the Gap45 domain. The lemma depends on the identical statement already present in Gap45.Beat.lag_q. It carries the @[simp] attribute so that Lean simplification tactics can rewrite the fraction automatically.
proof idea
The proof is a one-line wrapper that invokes the norm_num tactic to reduce both sides of the rational equality to a common normal form.
why it matters
The result supplies a concrete numerical identity that the downstream lag_q in Gap45.Beat can invoke under simp. Within the Recognition framework it closes a minor computational step required for exact fraction handling in Gap45 derivations, without touching phi-ladder or T0-T8 landmarks directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.