sync_prime_factorization
plain-language theorem explainer
The theorem states that the synchronization period equals 360 expressed as its prime factorization 2 cubed times 3 squared times 5. Researchers citing the Gap-45 synchronization argument for forcing spatial dimension D equals 3 would reference this factorization to connect the lcm to the 360-degree periodicity of SO(3). The proof is a one-line term that unfolds the three definitions and closes by reflexivity.
Claim. Let $p$ be the least common multiple of the eight-tick period and the gap-45 parameter. Then $p = 2^3 3^2 5$.
background
The module proves that spatial dimension D equals 3 is forced by the RS framework via four arguments, one of which is the Gap-45 / 8-Tick Synchronization. eight_tick is defined as the eight-tick period (2^D for ledger coverage with D=3). gap_45 is the integration gap parameter D squared times (D plus 2) evaluated at D=3, yielding 45. sync_period is defined as Nat.lcm eight_tick gap_45, which equals 360 by the physical motivation that 45 is the cumulative phase accumulation over a closed 8-tick cycle (fence-post principle: 8 ticks plus 1 for closure gives the 9th triangular number). Upstream results supply the same eight_tick and sync_period definitions in Gap45.PhysicalMotivation and RRF.Foundation.Constants, confirming the lcm identity.
proof idea
The term proof unfolds sync_period, eight_tick, and gap_45, then applies reflexivity to obtain the equality 360 = 2^3 * 3^2 * 5.
why it matters
This declaration supplies the explicit prime factorization inside the synchronization condition lcm(8,45)=360 that appears in the Gap-45 / 8-Tick Synchronization argument for forcing D=3 (see MODULE_DOC). It directly supports the claim that 360 degrees in a full rotation relates to SO(3) periodicity and the eight-tick octave (T7) from the forcing chain. No downstream theorems are recorded yet, so the result currently serves as a verified intermediate identity rather than a parent for further derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.