phasePeriod_even_8
plain-language theorem explainer
phasePeriod_even_8 shows that the triangular number T(64) is even. Researchers studying dimensional rigidity and the selection of D=3 for minimal synchronization periods cite it to confirm that even dimensions produce partial period alignment. The proof is a direct numerical check via native_decide on the definition phasePeriod(D) = T(D²).
Claim. $2$ divides $T(64)$, where $T(n) = n(n+1)/2$ is the $n$th triangular number and phasePeriod$(D) := T(D^2)$.
background
The module formalizes constraint (S) from the Dimensional Rigidity paper: among odd spatial dimensions $D ≥ 3$, $D=3$ uniquely minimizes the synchronization period lcm$(2^D, T(D^2))$. phasePeriod is the sibling definition phasePeriod$(D) := T(D^2)$, with $T$ the triangular-number function. For even $D$, $T(D^2)$ is even, so gcd$(2^D, T(D^2)) > 1$ and the periods partially align.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate phasePeriod 8 and test divisibility by 2.
why it matters
The result supplies the even-D evenness fact used in the module's argument that only odd $D$ yields full coprimality and that $D=3$ therefore gives the global minimum sync period of 360. It directly supports the claim that even dimensions reduce the uncomputability barrier via partial alignment with the 8-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.