lag_r
plain-language theorem explainer
Gap45 time-lag calculations rely on the identity 45 over 8 times 120 equaling 3 over 64 in the reals. This simplification lemma is referenced by the Beat module for arithmetic reductions. The proof reduces immediately via the norm_num tactic without additional lemmas.
Claim. $45 / (8 * 120) = 3 / 64$ holds over the real numbers.
background
The TimeLag submodule of Gap45 handles time-lag computations, with module documentation stating the equality as rationals. This lemma lifts the relation to reals. It depends on the matching lag_r lemma from the Beat submodule, which encodes the identical numerical identity.
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to normalize the arithmetic expression and discharge the equality.
why it matters
This lemma supplies the arithmetic fact required by the parent lag_r declaration in the Beat module. It supports precise time-lag modeling inside the Gap45 domain of the Recognition Science framework, consistent with the eight-tick octave. No open questions on constants or the Recognition Composition Law are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.