  35/-! ## Triangular Numbers -/
  36
  37/-- The n-th triangular number: T(n) = n(n+1)/2. -/
  38def T (n : ℕ) : ℕ := n * (n + 1) / 2
  39
  40@[simp] theorem T_0 : T 0 = 0 := rfl
  41@[simp] theorem T_1 : T 1 = 1 := rfl
  42@[simp] theorem T_9 : T 9 = 45 := by native_decide
  43@[simp] theorem T_25 : T 25 = 325 := by native_decide
  44@[simp] theorem T_49 : T 49 = 1225 := by native_decide
  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. -/

papers checked against this theorem

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