Nicomachus's theorem and its generalizations

DefinitionNicomachean defect#✓fully proved

For a finite sequence \(\sigma = (a_1, \ldots, a_n)\) of elements of a commutative ring, the Nicomachean defect of \(\sigma\) is \(\nu(\sigma) = \left(\sum_{i=1}^n a_i\right)^2 - \sum_{i=1}^n a_i^3\).

def nicomacheanNu {R : Type*} [CommRing R] (σ : List R) : R :=
  σ.sum ^ 2 - (σ.map (· ^ 3)).sum
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, Translations and Extensions of the Nicomachean Identity, Journal of Integer Sequences 27 (2024), Article 24.6.3, Section 1.
Used by 9
Used byGolden-ratio sequences with vanishing Nicomachean defect · Nicomachean families sharing a quadratic factor · Nicomachean sequences with a large gap at the top · Nicomachean sequences of rationals with large denominators · Two-valued Nicomachean sequences with a large gap · Adjoined Nicomachean sequences are eventually arithmetic progressions · Second differences of roots of translated Nicomachean bag squares · Examples of the Nicomachean defect · Generating functions for run-and-repeat Nicomachean sequences

TheoremExamples of the Nicomachean defect#✓fully proved

For the Nicomachean defect \(\nu\) of a sequence of integers, \(\nu(1, 2, 3, 4) = 0\), \(\nu(1, 2) = 0\), \(\nu(3, 3, 3) = 0\), \(\nu(1, 2, 2, 3, 4, 5, 6, 8) = 0\) and \(\nu(1, 2, 2, 3, 4, 6, 6, 8) = -28\).

The last two are the values at \(x = 5\) and \(x = 6\) of the paper's identity \(\nu(1, 2, 2, 3, 4, x, 6, 8) = (5 - x)(x - 4)(8 + x)\); the identity itself is not stated here.

theorem nicomacheanNu_examples :
    nicomacheanNu ([1, 2, 3, 4] : List ℤ) = 0 ∧ nicomacheanNu ([1, 2] : List ℤ) = 0 ∧
      nicomacheanNu ([3, 3, 3] : List ℤ) = 0 ∧
      nicomacheanNu ([1, 2, 2, 3, 4, 5, 6, 8] : List ℤ) = 0 ∧
      nicomacheanNu ([1, 2, 2, 3, 4, 6, 6, 8] : List ℤ) = -28
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, Translations and Extensions of the Nicomachean Identity, Journal of Integer Sequences 27 (2024), Article 24.6.3, Section 1.
Uses 1
Statement usesNicomachean defect

DefinitionThe Nicomachean progression factor#✓fully proved

For rational numbers \(n\), \(s\) and \(a\), define

\[\alpha(n, s, a) = 2n^2 + na - a^2 + \frac{n(n-1)(s - s^2)}{2} - (n-1)as.\]

This is the second factor of \(\nu(S_m)\), where \(\nu(a_1, \dots, a_k) = (a_1 + \dots + a_k)^2 - (a_1^3 + \dots + a_k^3)\) is the Nicomachean defect, \(S = (a, a + s, \dots, a + (n-1)s)\), and \(S_m\) joins \(n\) copies of \(n\) with the translated progressions \(S, S + n, \dots, S + mn\).

def nicomacheanAlpha (n s a : ℚ) : ℚ :=
  2 * n ^ 2 + n * a - a ^ 2 + n * (n - 1) * (s - s ^ 2) / 2 - (n - 1) * a * s
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, Translations and Extensions of the Nicomachean Identity, Journal of Integer Sequences 27 (2024), Article 24.6.3, Section 6, equation (nusm).
Used by 2
Used bySpecializations of the Nicomachean factor at \(s = 1, 2, 3\) · Positive integer roots of the Nicomachean factor for \(s = 1, 2\)

TheoremSpecializations of the Nicomachean factor at \(s = 1, 2, 3\)#✓fully proved

Let \(\alpha(n, s, a) = 2n^2 + na - a^2 + n(n-1)(s - s^2)/2 - (n-1)as\). For all rational numbers \(n\) and \(a\), \(\alpha(n, 1, a) = 2n^2 + a - a^2\), \(\alpha(n, 2, a) = n^2 + (1 - a)n - a^2 + 2a\) and \(\alpha(n, 3, a) = -(a + n - 3)(a + n)\).

theorem nicomacheanAlpha_one_two_three (n a : ℚ) :
    nicomacheanAlpha n 1 a = 2 * n ^ 2 + a - a ^ 2 ∧
      nicomacheanAlpha n 2 a = n ^ 2 + (1 - a) * n - a ^ 2 + 2 * a ∧
      nicomacheanAlpha n 3 a = -(a + n - 3) * (a + n)
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, Translations and Extensions of the Nicomachean Identity, Journal of Integer Sequences 27 (2024), Article 24.6.3, Section 6.
Uses 1
Statement usesThe Nicomachean progression factor

TheoremSecond differences of roots of translated Nicomachean bag squares#●ready to prove

Write \(\nu(a_1, \dots, a_k) = (a_1 + \dots + a_k)^2 - (a_1^3 + \dots + a_k^3)\) for the Nicomachean defect of a finite sequence. For natural numbers \(m\) let

\[t(m) = \frac{3(m^2 - 6m - 3) + \sqrt{3(m-1)^2(35m^2 + 34m + 11)}}{24},\]
\[s(m) = \frac{3(m^2 - 6m - 3) - \sqrt{3(m-1)^2(35m^2 + 34m + 11)}}{24},\]

let \(A_m^2\) be the sequence of the \(m^2\) products \(ij\) with \(1 \le i, j \le m\) (the bag square of \((1, 2, \dots, m)\)), let \(A_m^2 + x\) be the sequence obtained by adding \(x\) to every entry, and let \(\rho(m)\) be the supremum of the set of real \(x\) with \(\nu(A_m^2 + x) = 0\). Then, as \(m \to \infty\), the second differences \(t(m+2) - 2t(m+1) + t(m)\) and \(\rho(m+2) - 2\rho(m+1) + \rho(m)\) converge to \((3 + \sqrt{105})/12\), and \(s(m+2) - 2s(m+1) + s(m)\) converges to \((3 - \sqrt{105})/12\).

For \(m \ge 1\), \(\nu(A_m^2 + x)\) is a cubic polynomial in \(x\) with leading coefficient \(-m^2\), so \(\rho(m)\) is its largest real root.

public theorem_wanted nicomachean_bagSquare_root_secondDifference_tendsto :
    let t : ℕ → ℝ := fun m => (3 * ((m : ℝ) ^ 2 - 6 * m - 3) +
      Real.sqrt (3 * ((m : ℝ) - 1) ^ 2 * (35 * (m : ℝ) ^ 2 + 34 * m + 11))) / 24
    let s : ℕ → ℝ := fun m => (3 * ((m : ℝ) ^ 2 - 6 * m - 3) -
      Real.sqrt (3 * ((m : ℝ) - 1) ^ 2 * (35 * (m : ℝ) ^ 2 + 34 * m + 11))) / 24
    let ρ : ℕ → ℝ := fun m => sSup {x : ℝ | nicomacheanNu
      (((List.range' 1 m).flatMap fun i => (List.range' 1 m).map fun j => ((i * j : ℕ) : ℝ)).map
        (· + x)) = 0}
    Tendsto (fun m => t (m + 2) - 2 * t (m + 1) + t m) atTop (𝓝 ((3 + Real.sqrt 105) / 12)) ∧
      Tendsto (fun m => s (m + 2) - 2 * s (m + 1) + s m) atTop
        (𝓝 ((3 - Real.sqrt 105) / 12)) ∧
      Tendsto (fun m => ρ (m + 2) - 2 * ρ (m + 1) + ρ m) atTop (𝓝 ((3 + Real.sqrt 105) / 12))
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, Translations and Extensions of the Nicomachean Identity, Journal of Integer Sequences 27 (2024), Article 24.6.3, Proposition 1 (jis-2024-24.6.3-prop-1).
Uses 1
Statement usesNicomachean defect

TheoremNicomachean sequences of rationals with large denominators#●ready to prove

Write \(\nu(a_1, \dots, a_n) = (a_1 + \dots + a_n)^2 - (a_1^3 + \dots + a_n^3)\) for the Nicomachean defect of a finite sequence. For every natural number \(Q\) there is a finite sequence \(\sigma\) of positive rational numbers with \(\nu(\sigma) = 0\) having an entry whose denominator in lowest terms is greater than \(Q\).

public theorem_wanted exists_pos_rat_nicomacheanNu_eq_zero_large_den (Q : ℕ) :
    ∃ σ : List ℚ, (∀ x ∈ σ, 0 < x) ∧ nicomacheanNu σ = 0 ∧ ∃ x ∈ σ, Q < x.den
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, Translations and Extensions of the Nicomachean Identity, Journal of Integer Sequences 27 (2024), Article 24.6.3, Proposition 3 (jis-2024-24.6.3-prop-3).
Uses 1
Statement usesNicomachean defect

TheoremTwo-valued Nicomachean sequences with a large gap#●ready to prove

Write \(\nu(a_1, \dots, a_n) = (a_1 + \dots + a_n)^2 - (a_1^3 + \dots + a_n^3)\) for the Nicomachean defect of a finite sequence. For every real \(\varepsilon > 0\) there are integers \(0 < a < b\) and a finite sequence \(\sigma\) whose entries all equal \(a\) or \(b\), in which both \(a\) and \(b\) occur, such that \(\nu(\sigma) = 0\) and \((b - a)/L > 1 - \varepsilon\), where \(L\) is the length of \(\sigma\).

public theorem_wanted exists_two_valued_nicomachean_large_gap {ε : ℝ} (hε : 0 < ε) :
    ∃ a b : ℤ, 0 < a ∧ a < b ∧ ∃ σ : List ℤ, (∀ x ∈ σ, x = a ∨ x = b) ∧ a ∈ σ ∧ b ∈ σ ∧
      nicomacheanNu σ = 0 ∧ 1 - ε < ((b - a : ℤ) : ℝ) / σ.length
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, Translations and Extensions of the Nicomachean Identity, Journal of Integer Sequences 27 (2024), Article 24.6.3, Proposition 4 (jis-2024-24.6.3-prop-4).
Uses 1
Statement usesNicomachean defect

TheoremGenerating functions for run-and-repeat Nicomachean sequences#●ready to prove

For integers \(j, m \ge 1\) let \(\sigma(j, m)\) be the integer sequence \((1, 2, \ldots, j + 1, m, \ldots, m)\) in which \(m\) is repeated \(2j\) times, and let \(\nu\) denote the Nicomachean defect. Call \(j \ge 1\) admissible if \(\nu(\sigma(j, m)) = 0\) for some integer \(m \ge 1\), let \(j_k\) be the \(k\)-th smallest admissible integer (counting from \(k = 0\)), and let \(m_k = j_k + \lfloor \sqrt{2j_k^2 + 3j_k + 2} \rfloor\). Then \(\nu(\sigma(j_k, m_k)) = 0\) for every \(k\), and in the ring of formal power series over \(\mathbb{Z}\)

\[ (X - 1)(1 - 6X + X^2)(1 + 6X + X^2) \sum_{k \ge 0} j_k X^k = X^4 + X^3 - 19X^2 - 5X - 2 \]

and

\[ (1 - X)(1 - 6X + X^2)(1 + 6X + X^2) \sum_{k \ge 0} m_k X^k = 6(1 + X)^2. \]

For admissible \(j\) the square root is an integer and \(m = j + \sqrt{2j^2 + 3j + 2}\) is the positive root of \(\nu(\sigma(j, m)) = 0\) in \(m\), so these say that \((j_k)\) and \((m_k)\) have the generating functions \((x^4 + x^3 - 19x^2 - 5x - 2)/((x - 1)(1 - 6x + x^2)(1 + 6x + x^2))\) and \(6(1 + x)^2/((1 - x)(1 - 6x + x^2)(1 + 6x + x^2))\).

public theorem_wanted nicomachean_run_repeat_generatingFunctions :
    let P : ℕ → Prop := fun j => 0 < j ∧ ∃ m : ℤ, 0 < m ∧
      nicomacheanNu ((List.range' 1 (j + 1)).map (fun i : ℕ => (i : ℤ)) ++
        List.replicate (2 * j) m) = 0
    let J : ℕ → ℕ := Nat.nth P
    let M : ℕ → ℕ := fun k => J k + Nat.sqrt (2 * J k ^ 2 + 3 * J k + 2)
    (∀ k, nicomacheanNu ((List.range' 1 (J k + 1)).map (fun i : ℕ => (i : ℤ)) ++
        List.replicate (2 * J k) (M k : ℤ)) = 0) ∧
      (X - 1) * (1 - 6 * X + X ^ 2) * (1 + 6 * X + X ^ 2) * PowerSeries.mk (fun k => (J k : ℤ)) =
        X ^ 4 + X ^ 3 - 19 * X ^ 2 - 5 * X - 2 ∧
      (1 - X) * (1 - 6 * X + X ^ 2) * (1 + 6 * X + X ^ 2) * PowerSeries.mk (fun k => (M k : ℤ)) =
        6 * (1 + X) ^ 2
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, Translations and Extensions of the Nicomachean Identity, Journal of Integer Sequences 27 (2024), Article 24.6.3, Proposition 5 (jis-2024-24.6.3-prop-5).
Uses 1
Statement usesNicomachean defect

TheoremNicomachean sequences with a large gap at the top#●ready to prove

Write \(\nu(a_1, \dots, a_n) = (a_1 + \dots + a_n)^2 - (a_1^3 + \dots + a_n^3)\) for the Nicomachean defect of a finite sequence. For every natural number \(G\) there is a finite sequence \(\sigma\) of positive integers with \(\nu(\sigma) = 0\) and entries \(a < b\) of \(\sigma\) such that \(b\) is the largest entry of \(\sigma\) and occurs exactly once, every entry other than \(b\) is at most \(a\), and \(b - a > G\).

public theorem_wanted exists_nicomachean_large_top_gap (G : ℕ) :
    ∃ σ : List ℤ, (∀ x ∈ σ, 0 < x) ∧ nicomacheanNu σ = 0 ∧ ∃ a ∈ σ, ∃ b ∈ σ,
      σ.count b = 1 ∧ (∀ x ∈ σ, x ≤ b) ∧ a < b ∧ (∀ x ∈ σ, x ≠ b → x ≤ a) ∧ (G : ℤ) < b - a
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, Translations and Extensions of the Nicomachean Identity, Journal of Integer Sequences 27 (2024), Article 24.6.3, Proposition 6 (jis-2024-24.6.3-prop-6).
Uses 1
Statement usesNicomachean defect

TheoremGolden-ratio sequences with vanishing Nicomachean defect#●ready to prove

Let \(\varphi = (1 + \sqrt 5)/2\) be the golden ratio and write \(\nu(a_1, \dots, a_k) = (a_1 + \dots + a_k)^2 - (a_1^3 + \dots + a_k^3)\) for the Nicomachean defect of a finite sequence of real numbers. For every natural number \(N\) there is a finite sequence \(\sigma\) of positive real numbers, each of the form \(p + q\varphi\) with \(p, q \in \mathbb{Z}\), such that \(\nu(\sigma) = 0\), \(\sigma\) contains \(\varphi^{-n}\) for every \(1 \le n \le N\), and \(\sigma\) has a subsequence of irrational entries whose length is more than half the length of \(\sigma\).

public theorem_wanted exists_goldenRatio_nicomachean_sequence (N : ℕ) :
    ∃ σ : List ℝ, (∀ x ∈ σ, 0 < x ∧ ∃ p q : ℤ, x = p + q * Real.goldenRatio) ∧
      (∃ τ : List ℝ, τ.Sublist σ ∧ σ.length < 2 * τ.length ∧ ∀ x ∈ τ, Irrational x) ∧
      nicomacheanNu σ = 0 ∧ ∀ n ∈ Finset.Icc 1 N, Real.goldenRatio⁻¹ ^ n ∈ σ
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, Translations and Extensions of the Nicomachean Identity, Journal of Integer Sequences 27 (2024), Article 24.6.3, Proposition 7 (jis-2024-24.6.3-prop-7).
Uses 1
Statement usesNicomachean defect

TheoremAdjoined Nicomachean sequences are eventually arithmetic progressions#●ready to prove

Write \(\nu(a_1, \dots, a_n) = (a_1 + \dots + a_n)^2 - (a_1^3 + \dots + a_n^3)\) for the Nicomachean defect of a finite sequence. Let \((a_1, \dots, a_n)\) be a finite, possibly empty, sequence of real numbers and let \(x_1, x_2, x_3, \dots\) be nonzero real numbers with \(x_{j+1} \ne -x_j\) for every \(j \ge 1\). If \(\nu(a_1, \dots, a_n, x_1, \dots, x_l) = 0\) for every \(l \ge 1\), then \(x_{j+1} = x_j + 1\) for every \(j \ge 2\); that is, \(x_2, x_3, \dots\) is an arithmetic progression with difference \(1\).

public theorem_wanted nicomachean_adjoined_arithmeticProgression (a : List ℝ) (x : ℕ → ℝ)
    (hx : ∀ j, x j ≠ 0) (hneg : ∀ j, x (j + 1) ≠ -x j)
    (hν : ∀ l, nicomacheanNu (a ++ (List.range (l + 1)).map x) = 0) :
    ∀ j, 1 ≤ j → x (j + 1) = x j + 1
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, Translations and Extensions of the Nicomachean Identity, Journal of Integer Sequences 27 (2024), Article 24.6.3, Proposition 8 (jis-2024-24.6.3-prop-8).
Uses 1
Statement usesNicomachean defect

TheoremPositive integer roots of the Nicomachean factor for \(s = 1, 2\)#●ready to prove

Let \(\alpha(n, s, a) = 2n^2 + na - a^2 + n(n-1)(s - s^2)/2 - (n-1)as\) and let \(F_0 = 0\), \(F_1 = 1\), \(F_{k+2} = F_{k+1} + F_k\) be the Fibonacci numbers. Let \(n \ge 1\) be a natural number. Then \(\alpha(n, 1, h) = 0\) for some positive integer \(h\) if and only if \(2n^2 = k(k+1)\) for some natural number \(k\), that is, \(n^2\) is a triangular number; \(\alpha(n, 2, h) = 0\) for some positive integer \(h\) if and only if \(n = F_{2k}\) for some \(k \ge 1\); and if \(n = F_{2k}\) with \(k \ge 1\), then every positive integer \(h\) with \(\alpha(n, 2, h) = 0\) equals \(F_{2k-1} + 1\).

By the factor theorem, \(\alpha(n, s, h) = 0\) says that \(a - h\) divides \(\alpha(n, s, a)\) as a polynomial in \(a\). The case \(n = 0\) is excluded: \(\alpha(0, 2, a)\) has the root \(2\).

public theorem_wanted nicomacheanAlpha_posIntRoot_iff {n : ℕ} (hn : 1 ≤ n) :
    ((∃ h : ℕ, 0 < h ∧ nicomacheanAlpha n 1 h = 0) ↔ ∃ k : ℕ, 2 * n ^ 2 = k * (k + 1)) ∧
      ((∃ h : ℕ, 0 < h ∧ nicomacheanAlpha n 2 h = 0) ↔ ∃ k : ℕ, 1 ≤ k ∧ n = Nat.fib (2 * k)) ∧
      ∀ k h : ℕ, 1 ≤ k → n = Nat.fib (2 * k) → 0 < h → nicomacheanAlpha n 2 h = 0 →
        h = Nat.fib (2 * k - 1) + 1
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, Translations and Extensions of the Nicomachean Identity, Journal of Integer Sequences 27 (2024), Article 24.6.3, Proposition 9 (jis-2024-24.6.3-prop-9).
Uses 1
Statement usesThe Nicomachean progression factor

TheoremNicomachean families sharing a quadratic factor#●ready to prove

Write \(\nu(a_1, \dots, a_n) = (a_1 + \dots + a_n)^2 - (a_1^3 + \dots + a_n^3)\) for the Nicomachean defect of a finite sequence. For every natural number \(N\) there are finite sequences \(\sigma_1, \dots, \sigma_N\) of positive integers, pairwise distinct as multisets, and an integer \(c\) such that for every \(i\) we have \(\nu(\sigma_i) = 0\) and, for all integers \(a\) and \(b\), the sequence \((\sigma_i, a, b)\) obtained by appending \(a\) and \(b\) to \(\sigma_i\) satisfies \(\nu(\sigma_i, a, b) = -(a + b)(a^2 - ab + b^2 - a - b - 2c)\).

Since \(\nu(\sigma_i) = 0\), the identity forces \(c\) to be the sum of the entries of every \(\sigma_i\). Positivity of the entries, the paper's setting, excludes trivial families such as \((k, -k, 1)\).

public theorem_wanted exists_nicomachean_family_same_quadratic_factor (N : ℕ) :
    ∃ σ : Fin N → List ℤ, Function.Injective (fun i => (σ i : Multiset ℤ)) ∧ ∃ c : ℤ, ∀ i,
      (∀ x ∈ σ i, 0 < x) ∧ nicomacheanNu (σ i) = 0 ∧
        ∀ a b : ℤ, nicomacheanNu (σ i ++ [a, b]) = -(a + b) * (a ^ 2 - a * b + b ^ 2 - a - b - 2 * c)
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, Translations and Extensions of the Nicomachean Identity, Journal of Integer Sequences 27 (2024), Article 24.6.3, Proposition 12 (jis-2024-24.6.3-prop-12).
Uses 1
Statement usesNicomachean defect

DefinitionTriangular numbers as reals#✓fully proved

For a natural number \(m\), \(T_m = m(m+1)/2\) is the \(m\)-th triangular number, viewed as a real number.

noncomputable def nicomachusTriangular (m : ℕ) : ℝ := (m : ℝ) * ((m : ℝ) + 1) / 2
Used by 3
Used byThe even-case square \(R_{m,e}\) · The odd-case square \(R_{m,o}(x)\) · Kim–Stolarsky balanced quadratic sum

DefinitionThe odd-case cube sum \(L_{m,o}\)#✓fully proved

For a natural number \(m\) and a real number \(x\),

\[L_{m,o}(x) = \sum_{j=1}^{m} (2j - 1)^3 + x^3 + \sum_{j=2}^{m} \bigl((2j - 2) + (j - 1)x\bigr)^3.\]
def nicomachusLOdd (m : ℕ) (x : ℝ) : ℝ :=
  (∑ j ∈ Finset.Icc 1 m, (2 * (j : ℝ) - 1) ^ 3) + x ^ 3 +
    ∑ j ∈ Finset.Icc 2 m, ((2 * (j : ℝ) - 2) + ((j : ℝ) - 1) * x) ^ 3
Used by 1
Used byGeneralized Nicomachus identity, odd case

DefinitionThe odd-case square \(R_{m,o}(x)\)#✓fully proved

For a natural number \(m\) and a real number \(x\),

\[R_{m,o}(x) = \bigl(T_{2m-1} + (1 + T_{m-1})\,x\bigr)^2,\]

where \(T_n = n(n+1)/2\) is the \(n\)-th triangular number (for \(m = 0\) the indices \(2m - 1\) and \(m - 1\) are read as \(0\)).

noncomputable def nicomachusROdd (m : ℕ) (x : ℝ) : ℝ :=
  (nicomachusTriangular (2 * m - 1) +
    (1 + nicomachusTriangular (m - 1)) * x) ^ 2
Uses 1 · Used by 1
Statement usesTriangular numbers as reals
Used byGeneralized Nicomachus identity, odd case

DefinitionThe odd-case polynomial \(P_{m,o}\)#✓fully proved

For a natural number \(m\) and a real number \(x\),

\[P_{m,o}(x) = \sum_{j=0}^{m} (4j + 1 + jx) \bigl((j + 1)(j - 2) + j^2 x\bigr).\]
def nicomachusPOdd (m : ℕ) (x : ℝ) : ℝ :=
  ∑ j ∈ Finset.Icc 0 m,
    (4 * (j : ℝ) + 1 + (j : ℝ) * x) *
      (((j : ℝ) + 1) * ((j : ℝ) - 2) + (j : ℝ) ^ 2 * x)
Used by 1
Used byGeneralized Nicomachus identity, odd case

DefinitionThe even-case cube sum \(L_{m,e}\)#✓fully proved

For a natural number \(m\) and a real number \(x\),

\[L_{m,e}(x) = \sum_{j=1}^{m} (2j - 1)^3 + x^3 + \sum_{j=1}^{m} (2j + jx)^3.\]
def nicomachusLEven (m : ℕ) (x : ℝ) : ℝ :=
  (∑ j ∈ Finset.Icc 1 m, (2 * (j : ℝ) - 1) ^ 3) + x ^ 3 +
    ∑ j ∈ Finset.Icc 1 m, (2 * (j : ℝ) + (j : ℝ) * x) ^ 3
Used by 1
Used byGeneralized Nicomachus identity, even case

DefinitionThe even-case square \(R_{m,e}\)#✓fully proved

For a natural number \(m\) and a real number \(x\),

\[R_{m,e}(x) = \bigl(T_{2m} + (1 + T_m)\,x\bigr)^2,\]

where \(T_n = n(n+1)/2\) is the \(n\)-th triangular number.

noncomputable def nicomachusREven (m : ℕ) (x : ℝ) : ℝ :=
  (nicomachusTriangular (2 * m) +
    (1 + nicomachusTriangular m) * x) ^ 2
Uses 1 · Used by 1
Statement usesTriangular numbers as reals
Used byGeneralized Nicomachus identity, even case

DefinitionFaulhaber expansion of the odd-case polynomial#✓fully proved

For real numbers \(m\) and \(x\), let

\[\widetilde{P}(m, x) = -2(m + 1) - (9 + 2x) \, \frac{m(m+1)}{2} - 3 \cdot \frac{m(m+1)(2m+1)}{6} + (4 + 5x + x^2) \left(\frac{m(m+1)}{2}\right)^2.\]

This is the polynomial in \(m\) obtained from the sum defining the odd-case polynomial \(P_{m,o}(x)\) by the Faulhaber formulas for \(\sum_{j=0}^{m} j^p\) with \(p \le 3\); it agrees with \(P_{m,o}(x)\) at every natural number \(m\).

noncomputable def nicomachusPClosed (m x : ℝ) : ℝ :=
  (-2) * (m + 1) + (-9 - 2 * x) * (m * (m + 1) / 2) +
    (-3) * (m * (m + 1) * (2 * m + 1) / 6) +
      (4 + 5 * x + x ^ 2) * (m * (m + 1) / 2) ^ 2
Used by 1
Used byThe even-case polynomial \(P_{m,e}\)

DefinitionThe even-case polynomial \(P_{m,e}\)#✓fully proved

For a natural number \(m\) and a real number \(x\), \(P_{m,e}(x) = \widetilde{P}(-m - 1, x)\), where \(\widetilde{P}(m, x)\) is the Faulhaber expansion of the odd-case polynomial \(P_{m,o}(x)\) as a polynomial in \(m\) (the paper defines \(P_{m,e}(x)\) by substituting \(-m - 1\) for \(m\) in that expansion).

noncomputable def nicomachusPEven (m : ℕ) (x : ℝ) : ℝ :=
  nicomachusPClosed (-(m : ℝ) - 1) x
Uses 1 · Used by 1
Statement usesFaulhaber expansion of the odd-case polynomial
Used byGeneralized Nicomachus identity, even case

DefinitionThe Kim–Stolarsky convergents \(\alpha_k\)#✓fully proved

The rational numbers \(\alpha_k\), for natural numbers \(k\), are defined by \(\alpha_0 = 0\), \(\alpha_1 = 1\) and \(\alpha_{k+1} = \frac{15 + 7\alpha_k}{13 + 6\alpha_k}\) for \(k \ge 1\).

For \(k \ge 1\), \(\alpha_k\) is the continued-fraction convergent \([1; 6, 3, \ldots, 6, 3]\) with \(2k - 2\) partial quotients after the semicolon (Equation (12) of Kim and Stolarsky); the value \(\alpha_0 = 0\) is a placeholder.

def nicomachusAlpha : ℕ → ℚ
  | 0 => 0
  | 1 => 1
  | (k + 2) => (15 + 7 * nicomachusAlpha (k + 1)) /
      (13 + 6 * nicomachusAlpha (k + 1))
Used by 2
Used byThe convergents \(\alpha_k\) in terms of the integers \(u_k\) · Kim–Stolarsky balanced quadratic sum

DefinitionThe Kim–Stolarsky integers \(u_k\)#✓fully proved

For a natural number \(k\), \(u_k\) is the coefficient of \(x^{k-1}\) in the power series expansion over \(\mathbb{Q}\) of

\[\frac{1 + 502x + x^2}{(1 - x)(1 - 398x + x^2)}.\]

For \(k \ge 1\) these are the integers \(u_k\) of Proposition 1 of Kim and Stolarsky; for \(k = 0\) the exponent \(k - 1\) is read as \(0\), so \(u_0 = u_1 = 1\).

noncomputable def nicomachusU (k : ℕ) : ℚ :=
  PowerSeries.coeff (k - 1)
    ((1 + 502 * PowerSeries.X + PowerSeries.X ^ 2) *
      ((1 - PowerSeries.X) *
        (1 - 398 * PowerSeries.X + PowerSeries.X ^ 2))⁻¹)
Used by 4
Used byThe convergents \(\alpha_k\) in terms of the integers \(u_k\) · Closed form for the Kim–Stolarsky integers \(u_k\) · Recurrence for the Kim–Stolarsky integers \(u_k\) · Kim–Stolarsky balanced quadratic sum

TheoremGeneralized Nicomachus identity, odd case#●ready to prove

Let \(L_{m,o}\) be the odd-case cube sum, \(R_{m,o}\) the odd-case square and \(P_{m,o}\) the odd-case polynomial. For every natural number \(m \ge 2\) and every real number \(x\),

\[L_{m+1,o}(x) - R_{m+1,o}(x) = x \, P_{m,o}(x) - x^2 + x^3.\]
theorem_wanted nicomachusLOdd_sub_ROdd_succ_eq (m : ℕ) (hm : 2 ≤ m)
    (x : ℝ) :
    nicomachusLOdd (m + 1) x - nicomachusROdd (m + 1) x =
      x * nicomachusPOdd m x - x ^ 2 + x ^ 3
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, "A Balanced Three or More-term Generalization of Nicomachus' Identity", Theorem 1.
Uses 3
Statement usesThe odd-case cube sum \(L_{m,o}\) · The odd-case polynomial \(P_{m,o}\) · The odd-case square \(R_{m,o}(x)\)

TheoremGeneralized Nicomachus identity, even case#●ready to prove

Let \(L_{m,e}\) be the even-case cube sum, \(R_{m,e}\) the even-case square and \(P_{m,e}\) the even-case polynomial. For every natural number \(m \ge 2\) and every real number \(x\),

\[L_{m,e}(x) - R_{m,e}(x) = x \, P_{m,e}(x) - x^2 + x^3.\]
theorem_wanted nicomachusLEven_sub_REven_eq (m : ℕ) (hm : 2 ≤ m)
    (x : ℝ) :
    nicomachusLEven m x - nicomachusREven m x =
      x * nicomachusPEven m x - x ^ 2 + x ^ 3
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, "A Balanced Three or More-term Generalization of Nicomachus' Identity", Theorem 1.
Uses 3
Statement usesThe even-case cube sum \(L_{m,e}\) · The even-case polynomial \(P_{m,e}\) · The even-case square \(R_{m,e}\)

TheoremClosed form for the Kim–Stolarsky integers \(u_k\)#●ready to prove

Let \(u_k\) be the coefficient of \(x^{k-1}\) in the power series expansion of \((1 + 502x + x^2)/((1 - x)(1 - 398x + x^2))\). For every integer \(k \ge 1\),

\[u_k = \frac{5(10 - 3\sqrt{11})^{2k-1} + 5(10 + 3\sqrt{11})^{2k-1} - 56}{44}.\]
theorem_wanted nicomachusU_eq_closedForm (k : ℕ) (hk : 1 ≤ k) :
    (nicomachusU k : ℝ) =
      (5 * (10 - 3 * Real.sqrt 11) ^ (2 * k - 1) +
        5 * (10 + 3 * Real.sqrt 11) ^ (2 * k - 1) - 56) / 44
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, "A Balanced Three or More-term Generalization of Nicomachus' Identity", Proposition 1.
Uses 1
Statement usesThe Kim–Stolarsky integers \(u_k\)

TheoremRecurrence for the Kim–Stolarsky integers \(u_k\)#●ready to prove

Let \(u_k\) be the coefficient of \(x^{k-1}\) in the power series expansion of \((1 + 502x + x^2)/((1 - x)(1 - 398x + x^2))\). For every integer \(k \ge 1\),

\[u_{k+1} = 252 + 199u_k + 30\sqrt{(3 + 2u_k)(23 + 22u_k)}.\]
theorem_wanted nicomachusU_succ_eq (k : ℕ) (hk : 1 ≤ k) :
    (nicomachusU (k + 1) : ℝ) =
      252 + 199 * (nicomachusU k : ℝ) +
        30 * Real.sqrt ((3 + 2 * (nicomachusU k : ℝ)) *
          (23 + 22 * (nicomachusU k : ℝ)))
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, "A Balanced Three or More-term Generalization of Nicomachus' Identity", Proposition 1.
Uses 1
Statement usesThe Kim–Stolarsky integers \(u_k\)

TheoremThe convergents \(\alpha_k\) in terms of the integers \(u_k\)#●ready to prove

Let \(\alpha_k\) be the Kim–Stolarsky convergents, with \(\alpha_1 = 1\) and \(\alpha_{k+1} = (15 + 7\alpha_k)/(13 + 6\alpha_k)\) for \(k \ge 1\), and let \(u_k\) be the coefficient of \(x^{k-1}\) in the power series expansion of \((1 + 502x + x^2)/((1 - x)(1 - 398x + x^2))\). For every integer \(k \ge 1\),

\[\alpha_k = \frac{-1 + \sqrt{11 - \frac{10}{3 + 2u_k}}}{2}.\]
theorem_wanted nicomachusAlpha_eq (k : ℕ) (hk : 1 ≤ k) :
    (nicomachusAlpha k : ℝ) =
      (-1 + Real.sqrt (11 - 10 / (3 + 2 * (nicomachusU k : ℝ)))) / 2
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, "A Balanced Three or More-term Generalization of Nicomachus' Identity", Proposition 2.
Uses 2
Statement usesThe Kim–Stolarsky convergents \(\alpha_k\) · The Kim–Stolarsky integers \(u_k\)

TheoremKim–Stolarsky balanced quadratic sum#●ready to prove

Let \(k \ge 1\), let \(\alpha_k\) be the numbers of Equation (12) (so \(\alpha_1 = 1\) and \(\alpha_{k+1} = (15 + 7\alpha_k)/(13 + 6\alpha_k)\)), let \(u_k\) be the integers of Proposition 1, and let \(T_n = n(n+1)/2\). With \((a, b, c) = (1, \alpha_k, -(1 + \alpha_k))\) and \((d, e, f) = (-a, -c, -b)\) as in (17), for every natural number \(m\),

\[\sum_{j=1}^{m} (a + bj + cj^2)(d + ej + fj^2) = T_{m-1}\left(\frac{(1 + m)(2 - 3m^2)}{3(3 + 2u_k)} + (3 + 2m)\,T_{m-1}\right).\]
theorem_wanted sum_quadratic_mul_quadratic_eq (k : ℕ) (hk : 1 ≤ k)
    (m : ℕ) :
    (∑ j ∈ Finset.Icc 1 m,
      (1 + (nicomachusAlpha k : ℝ) * (j : ℝ) -
          (1 + (nicomachusAlpha k : ℝ)) * (j : ℝ) ^ 2) *
        (-1 + (1 + (nicomachusAlpha k : ℝ)) * (j : ℝ) -
          (nicomachusAlpha k : ℝ) * (j : ℝ) ^ 2)) =
      nicomachusTriangular (m - 1) *
        (((1 + (m : ℝ)) * (2 - 3 * (m : ℝ) ^ 2) /
          (3 * (3 + 2 * (nicomachusU k : ℝ)))) +
            (3 + 2 * (m : ℝ)) * nicomachusTriangular (m - 1))
Sources
  • Seon-Hong Kim and Kenneth B. Stolarsky, "A Balanced Three or More-term Generalization of Nicomachus' Identity", Theorem 2.
Uses 3
Statement usesThe Kim–Stolarsky convergents \(\alpha_k\) · Triangular numbers as reals · The Kim–Stolarsky integers \(u_k\)
14 fully proved15 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.