phasePeriod_even_4
plain-language theorem explainer
The theorem shows that the triangular number T(16) is even. Researchers on dimensional rigidity cite it to confirm that even D permit partial alignment between 2^D and T(D²), lowering the synchronization lcm. The result follows from direct evaluation of the definition via native decision.
Claim. $2$ divides the 16th triangular number, i.e., $2 | T(16)$ where $T(n) = n(n+1)/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²)). The function phasePeriod maps a dimension D to the triangular number T(D²). For even D the triangular number T(D²) is even, so gcd(2^D, T(D²)) > 1 and the periods partially align. Upstream, phasePeriod is defined directly as T(D * D).
proof idea
Native decide evaluates the definition of phasePeriod at input 4 to obtain T(16) and checks divisibility by 2 by direct arithmetic.
why it matters
This instance verifies the even-dimension case in the module's argument that only odd D yield full coprimality between 2^D and T(D²). It supports the claim that D = 3 gives the minimal sync period of 360 via T(9) = 45. The result connects to the eight-tick octave generalized to 2^D and the selection of D = 3 as the unique minimizer among odd dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.