constraint_S_minimization
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not define or derive the synchronization period function.
- Does not treat even dimensions where gcd($2^D$, $T(D^2)$) exceeds 1.
- Does not include $D=3$ itself in the quantified set.
- Does not address dimensions outside the listed odd values up to 11.
formal statement (Lean)
122theorem constraint_S_minimization :
123 ∀ D ∈ ({5, 7, 9, 11} : Finset ℕ), syncPeriod 3 < syncPeriod D := by
proof body
Term-mode proof.
124 intro D hD
125 fin_cases hD <;> native_decide
126
127/-- D = 3 is the unique minimizer: for all odd D with 3 ≤ D ≤ 11 and D ≠ 3,
128 the sync period at D strictly exceeds that at D = 3. -/