syncPeriod_5

formal source

  86def syncPeriod (D : ℕ) : ℕ := Nat.lcm (2^D) (phasePeriod D)
  87
  88@[simp] theorem syncPeriod_3 : syncPeriod 3 = 360 := by native_decide
  89@[simp] theorem syncPeriod_5 : syncPeriod 5 = 10400 := by native_decide
  90@[simp] theorem syncPeriod_7 : syncPeriod 7 = 156800 := by native_decide
  91@[simp] theorem syncPeriod_9 : syncPeriod 9 = 1700352 := by native_decide
  92@[simp] theorem syncPeriod_11 : syncPeriod 11 = 15116288 := by native_decide
  93
  94/-! ## The Minimization Theorem (Constraint S) -/
  95
  96/-- D = 3 has strictly smaller sync period than D = 5. -/
  97theorem sync_3_lt_5 : syncPeriod 3 < syncPeriod 5 := by native_decide
  98
  99/-- D = 3 has strictly smaller sync period than D = 7. -/
 100theorem sync_3_lt_7 : syncPeriod 3 < syncPeriod 7 := by native_decide
 101
 102/-- D = 3 has strictly smaller sync period than D = 9. -/
 103theorem sync_3_lt_9 : syncPeriod 3 < syncPeriod 9 := by native_decide
 104
 105/-- D = 3 has strictly smaller sync period than D = 11. -/
 106theorem sync_3_lt_11 : syncPeriod 3 < syncPeriod 11 := by native_decide
 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)