sync_3_lt_11
Among odd spatial dimensions D ≥ 3 the synchronization period lcm(2^D, T(D²)) is strictly smaller at D=3 than at D=11. Researchers formalizing dimensional selection in Recognition Science cite the result to justify why the 45-phase period is uniquely preferred. The proof is a direct native computation that evaluates the two concrete period values and confirms the inequality.
claim$lcm(2^3, T(9)) < lcm(2^{11}, T(121))$, where $T(n) = n(n+1)/2$ is the nth triangular number.
background
The module encodes constraint (S) from the Dimensional Rigidity paper: among odd D ≥ 3, D=3 uniquely minimizes the synchronization period lcm(2^D, T(D²)). The 8-tick period generalizes to 2^D while the parity matrix of the hypercube Q_D contributes D² entries whose cumulative phase is the triangular number T(D²). For odd D the triangular number is odd, guaranteeing coprimality with 2^D and therefore the full least-common-multiple cost.
proof idea
The proof is a one-line wrapper that applies native_decide to the concrete numerical values of the two synchronization periods.
why it matters in Recognition Science
The declaration supplies the concrete comparison that realizes constraint (S) and thereby explains the selection of the 45-phase period as T(9) at the minimizing dimension. It sits inside the forcing chain at the step that fixes D=3 and the eight-tick octave, and it supplies the numerical grounding for later mass-ladder and Berry-threshold arguments that presuppose the minimal synchronization cost.
scope and limits
- Does not treat even dimensions where gcd(2^D, T(D²)) > 1.
- Does not derive the lcm expression from the Recognition Composition Law.
- Does not prove global minimality over every odd D; only compares 3 and 11.
- Does not link the period value to any observable mass or coupling.
formal statement (Lean)
106theorem sync_3_lt_11 : syncPeriod 3 < syncPeriod 11 := by native_decide
proof body
Term-mode proof.
107
108/-- **CONSTRAINT (S)**: Among odd dimensions D ∈ {3,5,7,9,11},
109 D = 3 uniquely minimizes the synchronization period lcm(2^D, T(D²)).
110
111 This is the formalization of constraint (S) from the Dimensional Rigidity
112 paper (Washburn/Zlatanović/Allahyarov 2026). It answers:
113 "Why 45 specifically?" — because 45 = T(9) = T(3²) is the phase period
114 at the dimension that minimizes synchronization cost.
115
116 The sync periods grow super-exponentially:
117 - D=3: 360
118 - D=5: 10400 (28.9× larger)
119 - D=7: 156800 (435.6× larger)
120 - D=9: 1700352 (4723.2× larger)
121 - D=11: 15116288 (41989.7× larger) -/