cycles_of_45
plain-language theorem explainer
The lemma states that the minimal joint duration beats contains exactly eight 45-fold cycles. Synchronization constructors in the Gap45 module cite it when populating the canonical Sync record. The proof is a one-line simplification that reduces via the beats definition and the lcm division identity for 8 and 45.
Claim. The number of 45-fold cycles inside the minimal joint duration satisfies $beats / 45 = 8$.
background
The Gap45 module opens with the coprimeness of 9 and 5, which fixes the gcd and lcm relations among the 8-tick and 45-fold periods. beats is defined as their least common multiple (equal to 360). Sibling lemmas such as lcm_8_45_div_45 supply the exact division identity required here. Upstream structures from PhiForcingDerived and SpectralEmergence supply the J-cost and gauge-sector context in which these periodicities arise, while the module documentation anchors the arithmetic in the coprimeness fact.
proof idea
The proof is a one-line term-mode wrapper. It applies simp to the beats definition together with the lcm_8_45_div_45 lemma, which directly yields the quotient 8.
why it matters
This lemma supplies the cycles45 field of the canonical Sync definition inside the Beat namespace. It completes the arithmetic for the joint period that feeds the eight-tick octave (T7) and downstream mechanism-design constructions. The result closes a small but necessary gap in the Gap45 synchronization layer before ledger factorization and empirical-program checks are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.