phasePeriod_5

formal source

  53def phasePeriod (D : ℕ) : ℕ := T (D * D)
  54
  55@[simp] theorem phasePeriod_3 : phasePeriod 3 = 45 := by native_decide
  56@[simp] theorem phasePeriod_5 : phasePeriod 5 = 325 := by native_decide
  57@[simp] theorem phasePeriod_7 : phasePeriod 7 = 1225 := by native_decide
  58@[simp] theorem phasePeriod_9 : phasePeriod 9 = 3321 := by native_decide
  59@[simp] theorem phasePeriod_11 : phasePeriod 11 = 7381 := by native_decide
  60
  61/-- For even D, T(D²) is even: no coprimality with 2^D. Verified for D ∈ {2,4,6,8,10}. -/
  62theorem phasePeriod_even_2 : 2 ∣ phasePeriod 2 := by native_decide
  63theorem phasePeriod_even_4 : 2 ∣ phasePeriod 4 := by native_decide
  64theorem phasePeriod_even_6 : 2 ∣ phasePeriod 6 := by native_decide
  65theorem phasePeriod_even_8 : 2 ∣ phasePeriod 8 := by native_decide
  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)