sync_3_lt_7
plain-language theorem explainer
The synchronization period for three spatial dimensions is strictly smaller than for seven dimensions. Researchers formalizing dimensional selection in Recognition Science cite this to confirm D=3 minimizes lcm(2^D, T(D^2)) among odd D >= 3. The proof evaluates the concrete numerical inequality by direct native computation of the least-common-multiple expressions.
Claim. $syncPeriod(3) < syncPeriod(7)$, where $syncPeriod(D) := lcm(2^D, T(D^2))$ and $T(n) = n(n+1)/2$ denotes the triangular number.
background
The 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)). For dimension D the 8-tick period generalizes to 2^D while the parity matrix of the hypercube Q_D contributes the triangular number T(D^2). The upstream definition syncPeriod(D) := Nat.lcm (2^D) (phasePeriod D) implements this lcm directly; a sibling definition in Papers.DraftV1 fixes the second argument at 45 for the D=3 case.
proof idea
The proof is a one-line term that applies native_decide to evaluate the inequality between the concrete values lcm(8,45) and lcm(128,1225).
why it matters
This result fills the concrete comparison step inside the module argument that D=3 yields the minimal sync period of 360, thereby selecting the triangular number 45 that appears in the Recognition Composition Law and the eight-tick octave. It supports the claim that only odd D produces full coprimality between 2^D and T(D^2). No downstream theorems depend on it yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.