syncPeriod_minimized_at_three
plain-language theorem explainer
Among dimensions D ≥ 3, the synchronization period S(D) = 2^D · 45 is uniquely minimized at D = 3. Dimension-forcing and CRT verification arguments in Recognition Science cite this to lock the eight-tick register against the factor 45. Proof: closed form, write D = 3+k, compare powers of two (strict when k > 0).
Claim. For every natural number $D \ge 3$, the synchronization period satisfies $S(3) \le S(D)$, and $S(D) = S(3)$ implies $D = 3$, where $S(n) := 2^n \cdot 45$.
background
Recognition Science forces spatial dimension $D = 3$ (T8) and an eight-tick octave of period $2^3$ (T7). Synchronization must also clear a factor of 45 from the band/alpha structure, so the natural period is $S(D) = 2^D \cdot 45$ (equivalently an LCM of a power of two with 45). At $D = 3$ this is the RS-native constant 360.
This module packages the CRT-style comparison that pins $D = 3$ by minimizing that period. The local closed form $S(n) = 2^n \cdot 45$ is supplied by the sibling identity used throughout the proof; the constant case matches lcm(8, 45) = 360.
The standing hypothesis $D \ge 3$ is exactly the regime of the spatial forcing chain; lower $D$ are already excluded upstream.
proof idea
Constructor split: inequality, then uniqueness.
Inequality: rewrite both sides by the closed form $S(n) = 2^n \cdot 45$. From $D \ge 3$ obtain $D = 3+k$. Since $2^k \ge 1$, one has $2^3 \le 2^{3+k}$; multiply by 45 and transport back through the closed form (commuting the factors as needed).
Uniqueness: again $D = 3+k$. The zero case is $D = 3$. For successor $k$, $3 < 3+\mathrm{succ},k$ gives a strict power inequality $2^3 < 2^{3+\mathrm{succ},k}$ (base 2 > 1), hence after multiplying by 45 one gets $S(3) < S(D)$, contradicting equality.
why it matters
Unique-minimum half of the dimension CRT package: among candidate dimensions $D \ge 3$, the sync period is smallest exactly at the forced value $D = 3$ from T8. Siblings supply the numeric witness $S(3) = 360$ and the LCM characterizations (lcm of a power of two with 45 equals 360 only at exponent 3); together they close the verification that the eight-tick octave and the 45-factor lock uniquely in three spatial dimensions.
No downstream edges are recorded yet. Natural consumers are global consistency or "why $D = 3$" verification theorems that quote the minimized sync period. Framework landmarks hit directly: T7 (eight-tick), T8 ($D = 3$), and the RS-native sync period 360.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.