syncPeriod
plain-language theorem explainer
The synchronization period S(D) is the least common multiple of 2^D and 45. It is the arithmetic object used in dimensional-rigidity arguments that compare the D-cube tick lattice to a fixed odd factor 45. Anyone citing the Chinese-remainder forcing of spatial dimension three, or the RS-native value 360, depends on this quantity. The declaration is a one-line Nat.lcm definition.
Claim. For each natural number $D$, define the synchronization period by $S(D):=\mathrm{lcm}(2^D,45)$.
background
Recognition Science forces spatial dimension by the T0–T8 chain: T7 supplies the eight-tick octave (period $2^3$), and T8 forces $D=3$. The module Verification.DimensionCRT packages that forcing as pure arithmetic on least common multiples.
The synchronization period compares a pure power-of-two clock $2^D$ (vertices of the $D$-cube) against the fixed odd integer 45. Upstream constants already set $D:=3$ in both AlphaDerivation and GapDerivation. In RS-native units the specialized value $\mathrm{lcm}(8,45)=360$ is recorded as the working synchronization period.
Because 45 is odd it is coprime to every power of two, so the lcm collapses to a product; that identity is proved immediately downstream.
proof idea
Pure definition: bind $S(D)$ to Nat.lcm (2^D) 45. No proof obligations. Downstream, syncPeriod_eq_mul unfolds the definition, notes that 2 and 45 are coprime (hence $2^D$ and 45 remain coprime), and rewrites the lcm as the ordinary product $(2^D)\cdot 45$.
why it matters
This definition is the carrier for Chinese-remainder style dimension forcing inside DimensionCRT. Parent results syncPeriod_3_eq_360 and syncPeriod_minimized_at_three show that among all $D\ge 3$ the period is uniquely minimized at $D=3$ with value 360, packaging the 8↔45 hinge as an arithmetic lemma. RSNativeUnits records the same minimum as the constant 360 and proves it equals $\mathrm{lcm}(8,45)$. The construction sits exactly at the T7/T8 junction: the eight-tick octave meets the odd factor that selects three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.