D3_unique_minimizer
plain-language theorem explainer
D equals 3 uniquely minimizes the synchronization period among odd dimensions from 3 to 11. Researchers working on dimensional selection in Recognition Science cite the result to justify why three spatial dimensions minimize synchronization cost. The proof performs exhaustive case analysis on the finitely many candidate odd values of D, then reduces each inequality to a numerical check.
Claim. For every odd natural number $D$ with $3 ≤ D ≤ 11$ and $D ≠ 3$, the synchronization period at dimension 3 is strictly smaller than the synchronization period at dimension $D$, where the synchronization period equals lcm of $2^D$ and the triangular number $T(D^2)$ with $T(n) = n(n+1)/2$.
background
This 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)$). The triangular number $T(n)$ equals $n(n+1)/2$, the eight-tick period generalizes to $2^D$, and the parity matrix of the hypercube $Q_D$ supplies the cumulative phase $T(D^2)$. For odd $D$ the arguments remain coprime.
proof idea
The proof introduces $D$ together with the hypotheses that $D$ is odd, $3 ≤ D ≤ 11$, and $D ≠ 3$. It applies interval_cases to $D$ to split into subgoals for each odd integer in the closed interval. Each subgoal simplifies under the definitions of syncPeriod, phasePeriod, and $T$, after which native_decide confirms the concrete numerical inequality.
why it matters
The theorem supplies the D3_minimizes field inside the constraintS certificate. It thereby verifies the central step of the Dimensional Rigidity paper that selects $D = 3$ because it minimizes synchronization cost. In the Recognition framework the result supports the T7 eight-tick octave at its lowest value and accounts for the appearance of 45 as $T(9)$. It leaves open the extension beyond $D = 11$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.