phasePeriod_even_6
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 in Recognition Science
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.
scope and limits
- Does not prove evenness of phasePeriod for arbitrary even D.
- Does not compute the numerical value of phasePeriod 6.
- Does not address the minimization among odd dimensions.
formal statement (Lean)
64theorem phasePeriod_even_6 : 2 ∣ phasePeriod 6 := by native_decide