sync_counts
plain-language theorem explainer
The synchronization theorem asserts that the least common multiple of the 8-beat and 45-fold periods equals 360, with exact cycle counts of 45 and 8 respectively. Modelers of periodic alignments in Recognition Science cite it when deriving joint clock lags from the 45-gap arithmetic. The proof applies three precomputed lemmas on the LCM value and its quotients in a single exact constructor.
Claim. The minimal number of beats required to synchronize an 8-beat symmetry with a 45-fold symmetry satisfies $lcm(8,45)=360$, $lcm(8,45)/8=45$, and $lcm(8,45)/45=8$.
background
The Gap45 module examines arithmetic relations arising from the 45-gap in the Recognition Science phi-ladder. The 8-beat symmetry corresponds to the eight-tick octave while the 45-fold symmetry derives from the first conflict rung in the mass formula. Upstream lemmas establish the base LCM equality and the division results by direct computation using gcd properties and numerical evaluation.
proof idea
The proof is a term-mode exact application of the triple constructor to the three lemmas lcm_8_45_eq_360, lcm_8_45_div_8, and lcm_8_45_div_45. Each of those lemmas reduces the claim to a numerical identity verified by decide or simpa tactics.
why it matters
This result closes the synchronization requirement for the 45-gap arithmetic, feeding the beat-level clock-lag fraction δ_time = 45/960 = 3/64. It supports the eight-tick octave alignment in the forcing chain (T7) and the mass ladder construction. No open questions are directly addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.