phasePeriod_even_8
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 in Recognition Science
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.
scope and limits
- Does not prove evenness of T(D²) for arbitrary even D.
- Does not compute lcm(2^D, T(D²)) or the resulting sync period.
- Does not address the minimization argument among odd dimensions.
formal statement (Lean)
65theorem phasePeriod_even_8 : 2 ∣ phasePeriod 8 := by native_decide