sync_prime_factorization
plain-language theorem explainer
The synchronization period defined via least common multiple of the eight-tick cycle and gap-45 parameter equals 360 and factors as 2 cubed times 3 squared times 5. Researchers closing the dimension-forcing argument in Recognition Science would cite this identity to confirm the 360-degree periodicity that selects D equals 3. The proof is a one-line unfolding of the three definitions followed by reflexivity.
Claim. The least common multiple of the eight-tick period and the gap-45 parameter equals $2^3 times 3^2 times 5$.
background
In the Dimension Forcing module the eight-tick period is defined as the natural number 8, the gap-45 parameter is defined as the natural number 45, and the synchronization period is defined as their least common multiple. The module document states that this least common multiple equals 360 and supplies the physical motivation that 45 arises as the cumulative phase over a closed eight-tick cycle via the fence-post principle. Upstream definitions in PhysicalMotivation and Constants repeat the same eight-tick value and confirm the same least-common-multiple construction.
proof idea
The proof is a one-line wrapper that unfolds the definitions of the synchronization period, eight-tick period, and gap-45 parameter, then applies reflexivity.
why it matters
This identity supplies the explicit prime factorization required by the synchronization step that forces D equals 3 in the module's second argument. It sits inside the eight-tick octave (T7) and the spatial-dimension step (T8) of the forcing chain, confirming that the least common multiple yields the 360-degree period associated with SO(3). No downstream declarations are recorded, so the result functions as a terminal verification inside the dimension-forcing block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.