phasePeriod_odd_9
plain-language theorem explainer
The theorem establishes that the phase period for dimension 9 is odd. Researchers working on dimensional rigidity and synchronization minimization in Recognition Science cite it to confirm coprimality of T(81) with 2^9 in the lcm calculation. The result supports the claim that only odd D yields full period separation. The proof proceeds by direct evaluation of the triangular number via native_decide.
Claim. $¬ 2 ∣ T(81)$, where $T(n) = n(n+1)/2$ denotes the nth triangular number.
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²)). For dimension D the 8-tick period generalizes to 2^D while the parity matrix of the hypercube Q_D has D² entries, so the cumulative phase is the triangular number T(D²). phasePeriod D is defined as T(D * D). For odd D, T(D²) is odd, ensuring gcd(2^D, T(D²)) = 1.
proof idea
The proof is a direct computation that evaluates phasePeriod 9 = T(81) and checks divisibility by 2 using native_decide.
why it matters
This declaration verifies the oddness of T(81) for D=9, which is required to show that only odd dimensions produce full coprimality and that D=3 yields the minimal sync period of 360. It fills the concrete check inside the uniqueness argument for D=3 among odd dimensions and connects to the eight-tick octave (T8) and D=3 spatial dimensions in the forcing chain. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.