constraint_S_minimization

formal source

 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
 134
 135/-- Even dimensions fail coprimality: 2 | T(D²) when 2 | D, so the
 136    uncomputability barrier is weakened. Verified for D ∈ {2,4,6,8,10}. -/
 137theorem even_D_not_coprime :
 138    ∀ D ∈ ({2, 4, 6, 8, 10} : Finset ℕ),
 139    ¬ Nat.Coprime (2^D) (phasePeriod D) := by
 140  intro D hD
 141  fin_cases hD <;> native_decide
 142
 143/-! ## Monotonicity (sync period grows with D for odd D) -/
 144
 145/-- The sync period is strictly increasing along odd dimensions. -/
 146theorem sync_strictly_increasing_odd :
 147    syncPeriod 3 < syncPeriod 5 ∧
 148    syncPeriod 5 < syncPeriod 7 ∧
 149    syncPeriod 7 < syncPeriod 9 ∧
 150    syncPeriod 9 < syncPeriod 11 := by
 151  exact ⟨by native_decide, by native_decide, by native_decide, by native_decide⟩
 152