sync_factorization
plain-language theorem explainer
The theorem establishes that the synchronization period, defined as the least common multiple of the eight-tick period and the gap-45 parameter, equals their direct product. Researchers tracing the dimension-forcing argument in Recognition Science cite this step to confirm the numerical relation that yields the 360-unit cycle selecting D=3. The proof is a term-mode reduction that unfolds the three definitions and closes by reflexivity.
Claim. Let $p$ be the synchronization period defined by $p = {lcm}(8,45)$. Then $p = 8 × 45$.
background
The DimensionForcing module proves that spatial dimension D=3 is forced by the RS framework. One argument links the eight-tick cycle (2^D for ledger coverage at D=3) to the 45-tick cumulative phase (the ninth triangular number T(9) arising from the fence-post principle for cycle closure). The synchronization condition is the least common multiple of these two periods, which equals 360 and factors as 2^3 × 3^2 × 5, thereby identifying D=3 via the power-of-two factor.
proof idea
The term proof unfolds the definitions of the synchronization period, the eight-tick period, and the gap-45 parameter, then applies reflexivity. The accompanying comment records that gcd(8,45)=1, so the least common multiple equals the product.
why it matters
This identity supplies the numerical bridge between the eight-tick octave and the gap-45 parameter that forces D=3 in the dimension-forcing chain. It is invoked by the sync_factorization result in Gap45Degeneracy, which states the concrete equality 360=8×45. The step sits inside the synchronization argument of the module and connects to the eight-tick period and physical-motivation definitions imported from Gap45.PhysicalMotivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.