syncPeriod_7
plain-language theorem explainer
The synchronization period at seven dimensions evaluates to 156800. Researchers comparing synchronization costs across odd dimensions in the Dimensional Rigidity argument cite this value to confirm the growth away from the D=3 minimum. The result follows from direct numerical evaluation of the lcm expression via native decision procedures.
Claim. The synchronization period at dimension 7 equals 156800, where the period is defined as the least common multiple of $2^7$ and the triangular number $T(49)$.
background
In the Gap45 module the synchronization period for dimension D is defined as lcm(2^D, phasePeriod D), with phasePeriod D equal to the triangular number T(D^2). The module formalizes constraint (S) from the Dimensional Rigidity paper: among odd D ≥ 3 only D=3 minimizes this period, because T(D^2) is odd precisely when D is odd and the resulting lcm is smallest at D=3. Upstream, the RSNativeUnits version fixes the three-dimensional case at 360 while the DraftV1 version specializes the definition to lcm(2^D, 45).
proof idea
The theorem is a one-line wrapper that applies the native_decide tactic to evaluate the lcm expression for D=7.
why it matters
This value is used to exhibit the rapid growth of the synchronization period for D=7 relative to the 360 obtained at D=3, thereby supporting the module claim that D=3 uniquely minimizes synchronization cost. It fills the explicit numerical comparison for the next odd dimension after 5 in the argument that selects the eight-tick octave and D=3 within the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.