phasePeriod_even_6
plain-language theorem explainer
The declaration shows that phasePeriod 6 is even. Researchers verifying parity properties in the synchronization minimization argument for even dimensions cite it when confirming that T(D²) shares a factor with 2^D. The proof is a direct evaluation that applies native_decide to the definition of phasePeriod.
Claim. $2$ divides $T(36)$, 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²)). phasePeriod(D) computes the triangular number T(D²) that enters the lcm. For even D the triangular number T(D²) is even, so gcd(2^D, T(D²)) > 1 and the periods partially align.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate phasePeriod 6 and confirm divisibility by 2.
why it matters
The result supplies a concrete parity check used in the module's argument that only odd D yields full coprimality between 2^D and T(D²). It therefore supports the claim that D = 3 gives the minimal sync period of 360. The instance aligns with the eight-tick octave generalization to 2^D in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.