sync_3_lt_5
plain-language theorem explainer
The synchronization period at D=3 is strictly smaller than at D=5. Researchers working on dimensional rigidity in Recognition Science cite this to confirm that three dimensions minimize synchronization cost among odd D greater than or equal to 3. The proof is a direct native decision on the concrete natural-number comparison of the two lcm expressions.
Claim. $syncPeriod(3) < syncPeriod(5)$, where $syncPeriod(D) := lcm(2^D, T(D^2))$ and $T(n) = n(n+1)/2$ is the triangular number giving the cumulative phase for the parity matrix of the hypercube $Q_D$.
background
The SyncMinimization module formalizes constraint (S) from the Dimensional Rigidity paper: among odd spatial dimensions D greater than or equal to 3, D=3 uniquely minimizes the synchronization period lcm(2^D, T(D^2)). For each D the 8-tick period generalizes to 2^D while the parity matrix of Q_D contributes D^2 entries whose cumulative phase is the triangular number T(D^2); the sync period is then their lcm. Only odd D produces full coprimality because T(D^2) is odd precisely when D is odd.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the inequality between lcm(2^3, phasePeriod 3) and lcm(2^5, phasePeriod 5) by direct computation on the concrete natural numbers.
why it matters
This result supports the claim that D=3 minimizes synchronization cost, as required by constraint (S) in the Dimensional Rigidity paper (Washburn/Zlatanović/Allahyarov, 2026). It contributes to the Recognition Science framework landmarks T7 (eight-tick octave generalized to 2^D) and T8 (D=3 spatial dimensions) by showing the minimal sync period of 360 is selected at the lowest odd dimension. The declaration has no downstream uses yet but closes part of the uniqueness argument for the number 45.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.