syncPeriod_9
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove the global minimum over all dimensions.
- Does not compute values for even dimensions.
- Does not define or derive phasePeriod.
- Does not connect to J-cost, phi-ladder, or mass formulas.
formal statement (Lean)
91@[simp] theorem syncPeriod_9 : syncPeriod 9 = 1700352 := by native_decide