constraint_S_minimization
plain-language theorem explainer
The theorem proves that the synchronization period at dimension 3 is strictly smaller than at dimensions 5, 7, 9, or 11. Researchers on dimensional rigidity in Recognition Science cite this to justify selection of D=3 and the phase period 45. The proof reduces to exhaustive case analysis over the finite set of odd dimensions followed by direct numerical comparison of the lcm values.
Claim. For every odd dimension $D$ in the set {5, 7, 9, 11}, the synchronization period at $D=3$ is strictly smaller than the synchronization period at $D$, where the synchronization period at dimension $D$ equals 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$ at least 3, $D=3$ uniquely minimizes the synchronization period lcm($2^D$, $T(D^2)$). Here $T(n)$ is the triangular number $n(n+1)/2$, the 8-tick period generalizes to $2^D$, and the parity matrix of the hypercube $Q_D$ contributes the $D^2$ entries whose cumulative phase is $T(D^2)$. Only odd $D$ yields full coprimality because $T(D^2)$ is then odd. The concrete values are 360 at $D=3$, 10400 at $D=5$, 156800 at $D=7$, 1700352 at $D=9$, and 15116288 at $D=11$.
proof idea
The term-mode proof introduces the dimension $D$ together with its membership in the Finset, applies fin_cases to split into the four concrete cases, and resolves each case by native_decide which evaluates the lcm expressions and performs the inequality check.
why it matters
This theorem supplies constraint (S) from the Dimensional Rigidity paper and thereby explains why the phase period equals 45 = $T(9)$ at the minimizing dimension. It extends the eight-tick octave (period $2^3$) and the spatial dimension $D=3$ from the forcing chain to the general odd-$D$ setting. The result anchors the super-exponential growth of synchronization cost that selects $D=3$ over higher odd dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.