syncPeriod_5
plain-language theorem explainer
The theorem states that the synchronization period for dimension 5 equals 10400. Researchers comparing synchronization costs across odd dimensions in Recognition Science cite this value to quantify the increase from the D=3 minimum. The proof is a direct native evaluation of the lcm definition.
Claim. $syncPeriod(5) = 10400$, where $syncPeriod(D) := lcm(2^D, T(D^2))$ and $T(n) = n(n+1)/2$ denotes the triangular number.
background
The Gap45 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^2)). Here syncPeriod(D) is defined as Nat.lcm (2^D) (phasePeriod D), with phasePeriod supplying the triangular number T(D^2). The upstream RSNativeUnits definition fixes the D=3 case at lcm(8,45)=360, while the DraftV1 version hard-codes the 45 factor.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the lcm expression for D=5 directly.
why it matters
This instance supplies the explicit D=5 value required to demonstrate growth of the synchronization period in the module's minimization argument. It supports the selection of D=3 as the unique minimizer among odd dimensions, generalizing the eight-tick octave (T7) to 2^D while preserving the D=3 outcome from T8. The result feeds the paper's claim that only odd D yields full coprimality and thus the minimal uncomputability barrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.