phasePeriod_odd_3
The theorem shows that T(9) is odd. Researchers formalizing the Dimensional Rigidity constraint on synchronization periods would cite it to establish coprimality between the 8-tick octave and the phase period at D=3. The proof is a direct computational check that evaluates the triangular number and confirms its parity.
claimThe triangular number $T(9)=45$ is odd, i.e., $2$ does not divide $T(9)$.
background
The triangular number is defined by $T(n)=n(n+1)/2$. The phase period for dimension $D$ is then $T(D^2)$. The module formalizes constraint (S) from the Dimensional Rigidity paper: among odd spatial dimensions $D$ at least 3, only $D=3$ minimizes the synchronization period given by the least common multiple of $2^D$ and $T(D^2)$. For odd $D$ the triangular number $T(D^2)$ is odd, so the two periods are coprime and the lcm reaches its smallest value at $D=3$.
proof idea
This is a one-line wrapper that applies native_decide to compute $T(9)=45$ and verify that the result is odd.
why it matters in Recognition Science
It supplies the concrete parity fact needed for the argument that odd $D$ yields full coprimality in the lcm, which is minimized at $D=3$ with sync period 360. The result therefore supports the selection of 45 as the unique minimal value under the eight-tick octave and the $D=3$ spatial dimension fixed by the Recognition Science forcing chain.
scope and limits
- Does not prove the general statement that $T(D^2)$ is odd for every odd $D$.
- Does not compute or compare the lcm values for other dimensions.
- Does not address even dimensions or their partial alignment.
- Does not derive the eight-tick period or the definition of $T$.
formal statement (Lean)
69theorem phasePeriod_odd_3 : ¬ 2 ∣ phasePeriod 3 := by native_decide