phasePeriod
plain-language theorem explainer
The definition computes the phase period for a given spatial dimension as the triangular number of its square. Researchers working on synchronization minimization in the Dimensional Rigidity paper cite it to show that D equals 3 yields the shortest period among odd dimensions. It is implemented as a direct one-line application of the triangular number function.
Claim. For a spatial dimension $D$, the phase period is $T(D^2)$, where $T(n) = n(n+1)/2$.
background
The module formalizes constraint (S) from the Dimensional Rigidity paper, showing that among odd dimensions $D$ at least 3, $D$ equals 3 uniquely minimizes the synchronization period given by the least common multiple of $2^D$ and the phase period. The triangular number $T(n)$ equals $n$ times $(n+1)$ divided by 2, arising as the cumulative phase from the $D^2$ entries in the parity matrix of the hypercube $Q_D$ (module doc). Upstream, the triangular number definition in the same module specializes the fundamental periods abbrev from Breath1024.
proof idea
The definition is a one-line wrapper that applies the triangular number function $T$ to the square of the input dimension.
why it matters
This definition supplies the phase period value used in the ConstraintS_Cert structure that packages the full certificate for constraint (S), including the phase value 45 at $D$ equals 3 and the coprimality conditions for odd dimensions. It supports the paper claim that $D$ equals 3 gives the minimal sync period of 360. In the Recognition Science framework it connects to the generalization of the eight-tick octave to period $2^D$ and the forcing of $D$ equals 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.