`phasePeriod_even_8`

proved

show as: view math explainer →

module: IndisputableMonolith.Gap45.SyncMinimization
domain: Gap45
line: 65 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gap45.SyncMinimization on GitHub at line 65.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

phasePeriod IndisputableMonolith.Gap45.SyncMinimization

formal source

  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)
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.