syncPeriod_9
plain-language theorem explainer
Computation of the synchronization period at nine dimensions produces the value 1700352. Analysts of the dimensional rigidity constraint in Recognition Science reference this when tracking the growth of lcm(2^D, T(D²)) for odd D. The proof evaluates the definition directly via native_decide.
Claim. The synchronization period for dimension nine satisfies $lcm(2^9, T(81)) = 1700352$, where $T(n) = n(n+1)/2$ is the triangular number.
background
The module implements 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²)). The general definition is syncPeriod(D) := Nat.lcm (2^D) (phasePeriod D), where phasePeriod(D) equals the triangular number T(D²) arising from the parity matrix of the hypercube Q_D. This generalizes the eight-tick period 2^3 to arbitrary D, with full coprimality only when D is odd.
proof idea
A one-line wrapper applies native_decide to evaluate the least common multiple of 512 and T(81) from the definition of syncPeriod at D=9.
why it matters
The declaration supplies an explicit value for D=9 that supports the minimality argument of constraint (S) in the Dimensional Rigidity paper. It extends framework landmarks T7 (eight-tick octave generalized to 2^D) and T8 (D=3 selection) by quantifying synchronization cost growth for larger odd dimensions. No downstream uses are recorded, but the result reinforces why T(9)=45 yields the global minimum among odd D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.