`T_16`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gap45.SyncMinimization on GitHub at line 48.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  45@[simp] theorem T_81 : T 81 = 3321 := by native_decide
  46@[simp] theorem T_121 : T 121 = 7381 := by native_decide
  47@[simp] theorem T_4 : T 4 = 10 := by native_decide
  48@[simp] theorem T_16 : T 16 = 136 := by native_decide
  49
  50/-! ## Parity of T(D²) -/
  51
  52/-- T(D²) for a given dimension. -/
  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

papers checked against this theorem

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