syncPeriod
plain-language theorem explainer
The declaration defines the synchronization period for spatial dimension D as the least common multiple of 2^D and the triangular number T(D^2). Researchers formalizing dimensional selection in Recognition Science cite it when proving D=3 uniquely minimizes synchronization cost among odd dimensions. It is implemented as a direct one-line wrapper around Nat.lcm applied to 2^D and phasePeriod D.
Claim. The synchronization period for spatial dimension $D$ is defined as $S(D) := {lcm}(2^D, T(D^2))$, where $T(n) = n(n+1)/2$ denotes the $n$th triangular number.
background
In the Sync Period Minimization module the synchronization period captures the least common multiple between the generalized 8-tick period $2^D$ and the cumulative phase $T(D^2)$. The phasePeriod definition computes $T(D·D)$ from the $D^2$ entries of the parity matrix on the hypercube $Q_D$. The module setting states that only odd $D$ produces full coprimality because $T(D^2)$ is then odd.
proof idea
This is a one-line wrapper that applies Nat.lcm to the power $2^D$ and the result of phasePeriod D.
why it matters
This definition supplies the core object for the parent theorems constraint_S_minimization and D3_unique_minimizer, which establish that D=3 uniquely minimizes the synchronization period among odd dimensions up to 11. It formalizes constraint (S) from the Dimensional Rigidity paper, answering why 45 is selected as T(9) at the minimizing dimension. In the Recognition framework it connects the eight-tick octave (T7) generalized to $2^D$ with the selection of D=3 spatial dimensions (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.