phasePeriod_even_2
plain-language theorem explainer
The theorem confirms that the phase period at dimension 2 is even, so T(4) shares a factor of 2 with the 2^D tick length. Researchers tracing the uniqueness of D=3 in synchronization minimization cite this to separate even and odd cases. The proof is a direct computational check on the concrete value T(4)=10.
Claim. $2$ divides the triangular number $T(4)$, where $T(n)=n(n+1)/2$.
background
The module formalizes constraint (S) from the Dimensional Rigidity paper: the synchronization period is lcm(2^D, T(D²)) and is minimized only at odd D=3. Here T(n) is the triangular number n(n+1)/2, and phasePeriod(D) is defined as T(D*D). The upstream definition phasePeriod simply composes T with dimension squaring. For even D the module notes that T(D²) is even, so gcd(2^D, T(D²))>1 and the periods partially align.
proof idea
One-line wrapper that applies native_decide to the concrete instance 2 | T(4).
why it matters
The result supplies the even-D verification step required by the module argument that only odd dimensions yield full coprimality between 2^D and T(D²). It therefore supports the claim that D=3 produces the shortest sync period (lcm(8,45)=360) among odd D>=3. No downstream uses are recorded; the fact closes the parity check for the even case in the paper's minimization analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.