sync_strictly_increasing_odd

formal source

 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
 153/-! ## Complete Certificate -/
 154
 155/-- The full constraint (S) certificate packaging the dimensional selection of 45. -/
 156structure ConstraintS_Cert where
 157  phase_at_D3 : phasePeriod 3 = 45
 158  sync_at_D3 : syncPeriod 3 = 360
 159  coprime_at_D3 : Nat.Coprime (2^3) (phasePeriod 3)
 160  even_D_fails : ∀ D ∈ ({2, 4, 6, 8, 10} : Finset ℕ),
 161    ¬ Nat.Coprime (2^D) (phasePeriod D)
 162  D3_minimizes : ∀ D : ℕ, D % 2 = 1 → 3 ≤ D → D ≤ 11 → D ≠ 3 →
 163    syncPeriod 3 < syncPeriod D
 164  monotone_odd : syncPeriod 3 < syncPeriod 5 ∧
 165    syncPeriod 5 < syncPeriod 7 ∧
 166    syncPeriod 7 < syncPeriod 9 ∧
 167    syncPeriod 9 < syncPeriod 11
 168
 169/-- The verified constraint (S) certificate. -/
 170def constraintS : ConstraintS_Cert where
 171  phase_at_D3 := by native_decide
 172  sync_at_D3 := by native_decide
 173  coprime_at_D3 := by native_decide
 174  even_D_fails := even_D_not_coprime
 175  D3_minimizes := D3_unique_minimizer
 176  monotone_odd := sync_strictly_increasing_odd