phasePeriod_odd_3

formal source

  66theorem phasePeriod_even_10 : 2 ∣ phasePeriod 10 := by native_decide
  67
  68/-- For odd D, T(D²) is odd. -/
  69theorem phasePeriod_odd_3 : ¬ 2 ∣ phasePeriod 3 := by native_decide
  70theorem phasePeriod_odd_5 : ¬ 2 ∣ phasePeriod 5 := by native_decide
  71theorem phasePeriod_odd_7 : ¬ 2 ∣ phasePeriod 7 := by native_decide
  72theorem phasePeriod_odd_9 : ¬ 2 ∣ phasePeriod 9 := by native_decide
  73theorem phasePeriod_odd_11 : ¬ 2 ∣ phasePeriod 11 := by native_decide
  74
  75/-! ## Coprimality with 2^D -/
  76
  77theorem coprime_3 : Nat.Coprime (2^3) (phasePeriod 3) := by native_decide
  78theorem coprime_5 : Nat.Coprime (2^5) (phasePeriod 5) := by native_decide
  79theorem coprime_7 : Nat.Coprime (2^7) (phasePeriod 7) := by native_decide
  80theorem coprime_9 : Nat.Coprime (2^9) (phasePeriod 9) := by native_decide
  81theorem coprime_11 : Nat.Coprime (2^11) (phasePeriod 11) := by native_decide
  82
  83/-! ## Sync Periods -/
  84
  85/-- The synchronization period for dimension D. -/
  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. -/