sync_3_lt_9

formal source

 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)
 120    - D=9:  1700352    (4723.2× larger)
 121    - D=11: 15116288   (41989.7× larger) -/
 122theorem constraint_S_minimization :
 123    ∀ D ∈ ({5, 7, 9, 11} : Finset ℕ), syncPeriod 3 < syncPeriod D := by
 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. -/
 129theorem D3_unique_minimizer :
 130    ∀ D : ℕ, D % 2 = 1 → 3 ≤ D → D ≤ 11 → D ≠ 3 →
 131    syncPeriod 3 < syncPeriod D := by
 132  intro D hodd hge hle hne
 133  interval_cases D <;> simp_all [syncPeriod, phasePeriod, T] <;> native_decide