delta_time_eq_3_div_64
plain-language theorem explainer
The equality establishes the clock-lag fraction for the 45-gap arithmetic as 3/64 in rational units. Modelers of beat synchronization between 8-cycle and 45-fold patterns cite this reduction. The proof reduces the rational equality by direct numerical normalization.
Claim. The beat-level clock-lag fraction for the 45-gap satisfies $45/960 = 3/64$.
background
Gap45 develops arithmetic for joint 8-beat cycles and 45-fold patterns. The minimal joint duration is the least common multiple of 8 and 45. The module opens by noting that 9 and 5 are coprime, which structures the 45-fold relations. Upstream results supply a meta-realization certificate recording required structural properties for self-reference and an explicit log-derivative bound that yields a known angular Lipschitz constant on the circle.
proof idea
The proof applies the norm_num tactic to simplify the rational arithmetic directly and confirm the equality.
why it matters
This identity supplies the explicit lag fraction inside the Gap45 beat-level API. It supports arithmetic steps connected to the eight-tick octave in the forcing chain. The result closes a basic reduction without new hypotheses or open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.