phasePeriod_even_2
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 in Recognition Science
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.
scope and limits
- Does not prove T(D²) even for arbitrary even D.
- Does not compute any lcm synchronization period.
- Does not treat odd dimensions or the D=3 minimum.
- Does not reference the Recognition Science forcing chain or constants.
formal statement (Lean)
62theorem phasePeriod_even_2 : 2 ∣ phasePeriod 2 := by native_decide