sync_factorization
plain-language theorem explainer
The theorem shows that the synchronization period, defined via least common multiple of the eight-tick cycle and gap-45 parameter, equals their direct product 360. Dimension-forcing arguments in Recognition Science cite this identity to anchor the 360-degree periodicity that selects D=3. The proof is a one-line wrapper that unfolds the three definitions and closes by reflexivity.
Claim. Let $P$ denote the synchronization period $P = {lcm}(8,45)$. Then $P = 8 times 45$.
background
The module DimensionForcing proves that spatial dimension D=3 is forced by the RS framework. It links the eight-tick cycle (2^D for ledger coverage at D=3) to the gap-45 parameter (the integration gap D^2(D+2) evaluated at D=3). The synchronization period is defined as the least common multiple of these two quantities. MODULE_DOC states that this lcm equals 360 and supplies the physical motivation: 45 is the cumulative phase accumulation over a closed 8-tick cycle via the fence-post principle.
proof idea
The proof is a one-line wrapper. It unfolds the definitions of sync_period (Nat.lcm eight_tick gap_45), eight_tick (8), and gap_45 (45), then applies reflexivity. The inline comments note that gcd(8,45)=1 so the lcm identity reduces to the product.
why it matters
This identity closes the Gap-45 / 8-Tick Synchronization argument for D=3 inside the four arguments of MODULE_DOC. It is used by the duplicate statement in Gap45Degeneracy and supports the downstream claim that 360 = 2^3 times 3^2 times 5, which isolates the factor 2^3 and thereby forces D=3. The result sits inside the T7 eight-tick octave and T8 D=3 steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.