Additive uniqueness of multiplicative functions

TheoremMultiplicative functions additive on pairs of squares#●ready to prove

Let \(f\) be a complex-valued multiplicative arithmetic function (so \(f(1) = 1\) and \(f(ab) = f(a) f(b)\) for coprime \(a\) and \(b\)) such that \(f(m^2 + n^2) = f(m^2) + f(n^2)\) for all positive integers \(m\) and \(n\). Then \(f(4)\) is \(0\) or \(4\); \(f(q^{2k}) = f(q^2)^k\) for all positive integers \(q\) and \(k\); and if \(f(4) = 4\), then \(f(m^2) = m^2\) for every positive integer \(m\).

The source also assumes \(f \ne 0\), which follows from \(f(1) = 1\).

public theorem_wanted multiplicative_additive_on_squares (f : ArithmeticFunction ℂ)
    (hf : f.IsMultiplicative)
    (hadd : ∀ m n : ℕ, 0 < m → 0 < n → f (m ^ 2 + n ^ 2) = f (m ^ 2) + f (n ^ 2)) :
    (f 4 = 0 ∨ f 4 = 4) ∧
      (∀ q k : ℕ, 0 < q → 0 < k → f (q ^ (2 * k)) = f (q ^ 2) ^ k) ∧
      (f 4 = 4 → ∀ m : ℕ, 0 < m → f (m ^ 2) = (m : ℂ) ^ 2)

Sources

Elchin Hasanalizade, On the k-Additive Uniqueness of Sums of Consecutive Squares for Multiplicative Functions, INTEGERS 25 (2025), Article A40, Theorem 1.

TheoremSums of consecutive squares form a \(k\)-additive uniqueness set for every \(k \ge 2\)#●ready to prove

Let \(k \ge 2\), and call a natural number a sum of consecutive squares if it equals \((n+1)^2 + (n+2)^2 + \dots + m^2\) for some natural numbers \(n < m\). Let \(f\) be a complex-valued multiplicative arithmetic function (so \(f(1) = 1\) and \(f(ab) = f(a) f(b)\) for coprime \(a\) and \(b\)). If \(f(x_1 + \dots + x_k) = f(x_1) + \dots + f(x_k)\) for all sums of consecutive squares \(x_1, \dots, x_k\), then \(f(n) = n\) for every natural number \(n\).

public theorem_wanted consecutiveSquareSums_kAdditiveUniqueness (k : ℕ) (hk : 2 ≤ k)
    (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ x : Fin k → ℕ, (∀ i, ∃ m n : ℕ, n < m ∧ x i = ∑ j ∈ Finset.Ioc n m, j ^ 2) →
      f (∑ i, x i) = ∑ i, f (x i)) :
    ∀ n : ℕ, f n = n

Sources

Elchin Hasanalizade, On the k-Additive Uniqueness of Sums of Consecutive Squares for Multiplicative Functions, INTEGERS 25 (2025), Article A40, Theorem 2.

DefinitionSums of two positive triangular numbers#✓fully proved

A natural number \(n\) is a sum of two positive triangular numbers if there are natural numbers \(a \ge 1\) and \(b \ge 1\) with \(2n = a(a+1) + b(b+1)\), that is, \(n = \frac{a(a+1)}{2} + \frac{b(b+1)}{2}\).

def IsSumTwoPositiveTriangular (n : ℕ) : Prop :=
  ∃ a b : ℕ, 1 ≤ a ∧ 1 ≤ b ∧ 2 * n = a * (a + 1) + b * (b + 1)

Used by 5

Used byPark's theorem on multiplicative functions additive on sums of two triangular numbers · Park's Lemma 2: the identity up to 21 when the value at 2 is nonzero · Park's Lemma 3: vanishing from 4 to 21 when the value at 2 is zero and at 3 is not · Park's Lemma 4: vanishing from 2 to 21 except at 5 · Park's Lemma 5: vanishing from 2 to 21 when the values at 2, 3 and 5 are zero

TheoremPark's theorem on multiplicative functions additive on sums of two triangular numbers#●ready to prove

Let \(f\) be a multiplicative arithmetic function with values in \(\mathbb{C}\) (so \(f\) is defined on the natural numbers with \(f(0) = 0\)) such that \(f(a + b) = f(a) + f(b)\) whenever \(a\) and \(b\) are both sums of two positive triangular numbers. Then either \(f(n) = n\) for every natural number \(n\), or \(f(n) = 0\) for every natural number \(n \notin \{1, 3, 5\}\) and \(f(3) f(5) = 0\).

theorem_wanted multiplicative_additive_on_sum_two_triangular_classification
    (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ a b : ℕ, IsSumTwoPositiveTriangular a →
      IsSumTwoPositiveTriangular b → f (a + b) = f a + f b) :
    (∀ n : ℕ, f n = (n : ℂ)) ∨
      ((∀ n : ℕ, n ≠ 1 ∧ n ≠ 3 ∧ n ≠ 5 → f n = 0) ∧ f 3 * f 5 = 0)

def IsSumTwoPositiveTriangular (n : ℕ) : Prop :=
  ∃ a b : ℕ, 1 ≤ a ∧ 1 ≤ b ∧ 2 * n = a * (a + 1) + b * (b + 1)

WantedExt/NumberTheory/ArithmeticFunction/MultiplicativeTriangularAdditiveWanted.lean:34

Sources

Poo-Sung Park, "Multiplicative Functions Additive on the Sums of Two Positive Triangular Numbers", Theorem 1.

Uses 1

Statement usesSums of two positive triangular numbers

TheoremPark's Lemma 2: the identity up to 21 when the value at 2 is nonzero#●ready to prove

Let \(f\) be a multiplicative arithmetic function with values in \(\mathbb{C}\) such that \(f(a + b) = f(a) + f(b)\) whenever \(a\) and \(b\) are both sums of two positive triangular numbers. If \(f(2) \neq 0\), then \(f(n) = n\) for every natural number \(n \le 21\).

theorem_wanted multiplicative_additive_on_sum_two_triangular_eq_id_le_21
    (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ a b : ℕ, IsSumTwoPositiveTriangular a →
      IsSumTwoPositiveTriangular b → f (a + b) = f a + f b)
    (hf2 : f 2 ≠ 0) :
    ∀ n : ℕ, n ≤ 21 → f n = (n : ℂ)

def IsSumTwoPositiveTriangular (n : ℕ) : Prop :=
  ∃ a b : ℕ, 1 ≤ a ∧ 1 ≤ b ∧ 2 * n = a * (a + 1) + b * (b + 1)

WantedExt/NumberTheory/ArithmeticFunction/MultiplicativeTriangularAdditiveWanted.lean:34

Sources

Poo-Sung Park, "Multiplicative Functions Additive on the Sums of Two Positive Triangular Numbers", Lemma 2.

Uses 1

Statement usesSums of two positive triangular numbers

TheoremPark's Lemma 3: vanishing from 4 to 21 when the value at 2 is zero and at 3 is not#●ready to prove

Let \(f\) be a multiplicative arithmetic function with values in \(\mathbb{C}\) such that \(f(a + b) = f(a) + f(b)\) whenever \(a\) and \(b\) are both sums of two positive triangular numbers. If \(f(2) = 0\) and \(f(3) \neq 0\), then \(f(n) = 0\) for every natural number \(n\) with \(4 \le n \le 21\).

theorem_wanted multiplicative_additive_on_sum_two_triangular_zero_of_three_ne_zero
    (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ a b : ℕ, IsSumTwoPositiveTriangular a →
      IsSumTwoPositiveTriangular b → f (a + b) = f a + f b)
    (hf2 : f 2 = 0) (hf3 : f 3 ≠ 0) :
    ∀ n : ℕ, 4 ≤ n → n ≤ 21 → f n = 0

def IsSumTwoPositiveTriangular (n : ℕ) : Prop :=
  ∃ a b : ℕ, 1 ≤ a ∧ 1 ≤ b ∧ 2 * n = a * (a + 1) + b * (b + 1)

WantedExt/NumberTheory/ArithmeticFunction/MultiplicativeTriangularAdditiveWanted.lean:34

Sources

Poo-Sung Park, "Multiplicative Functions Additive on the Sums of Two Positive Triangular Numbers", Lemma 3.

Uses 1

Statement usesSums of two positive triangular numbers

TheoremPark's Lemma 4: vanishing from 2 to 21 except at 5#●ready to prove

Let \(f\) be a multiplicative arithmetic function with values in \(\mathbb{C}\) such that \(f(a + b) = f(a) + f(b)\) whenever \(a\) and \(b\) are both sums of two positive triangular numbers. If \(f(2) = 0\) and \(f(5) \neq 0\), then \(f(n) = 0\) for every natural number \(n\) with \(2 \le n \le 21\) and \(n \neq 5\).

theorem_wanted multiplicative_additive_on_sum_two_triangular_zero_of_five_ne_zero
    (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ a b : ℕ, IsSumTwoPositiveTriangular a →
      IsSumTwoPositiveTriangular b → f (a + b) = f a + f b)
    (hf2 : f 2 = 0) (hf5 : f 5 ≠ 0) :
    ∀ n : ℕ, 2 ≤ n → n ≤ 21 → n ≠ 5 → f n = 0

def IsSumTwoPositiveTriangular (n : ℕ) : Prop :=
  ∃ a b : ℕ, 1 ≤ a ∧ 1 ≤ b ∧ 2 * n = a * (a + 1) + b * (b + 1)

WantedExt/NumberTheory/ArithmeticFunction/MultiplicativeTriangularAdditiveWanted.lean:34

Sources

Poo-Sung Park, "Multiplicative Functions Additive on the Sums of Two Positive Triangular Numbers", Lemma 4.

Uses 1

Statement usesSums of two positive triangular numbers

TheoremPark's Lemma 5: vanishing from 2 to 21 when the values at 2, 3 and 5 are zero#●ready to prove

Let \(f\) be a multiplicative arithmetic function with values in \(\mathbb{C}\) such that \(f(a + b) = f(a) + f(b)\) whenever \(a\) and \(b\) are both sums of two positive triangular numbers. If \(f(2) = f(3) = f(5) = 0\), then \(f(n) = 0\) for every natural number \(n\) with \(2 \le n \le 21\).

theorem_wanted multiplicative_additive_on_sum_two_triangular_zero_of_all_zero
    (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ a b : ℕ, IsSumTwoPositiveTriangular a →
      IsSumTwoPositiveTriangular b → f (a + b) = f a + f b)
    (hf2 : f 2 = 0) (hf3 : f 3 = 0) (hf5 : f 5 = 0) :
    ∀ n : ℕ, 2 ≤ n → n ≤ 21 → f n = 0

def IsSumTwoPositiveTriangular (n : ℕ) : Prop :=
  ∃ a b : ℕ, 1 ≤ a ∧ 1 ≤ b ∧ 2 * n = a * (a + 1) + b * (b + 1)

WantedExt/NumberTheory/ArithmeticFunction/MultiplicativeTriangularAdditiveWanted.lean:34

Sources

Poo-Sung Park, "Multiplicative Functions Additive on the Sums of Two Positive Triangular Numbers", Lemma 5.

Uses 1

Statement usesSums of two positive triangular numbers

TheoremAdditive uniqueness of generalized nonagonal numbers#●ready to prove

Let \(f\) be a multiplicative arithmetic function with values in \(\mathbb{C}\) such that \(f(a + b) = f(a) + f(b)\) for all positive integers \(a\) and \(b\) that are generalized nonagonal numbers, that is, \(2a = m(7m - 5)\) and \(2b = k(7k - 5)\) for some integers \(m\) and \(k\). Then \(f(n) = n\) for every natural number \(n\).

public theorem_wanted multiplicative_nonagonal_additive_eq_id
    (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ a b : ℕ, 0 < a → 0 < b →
      (∃ m : ℤ, 2 * (a : ℤ) = m * (7 * m - 5)) → (∃ m : ℤ, 2 * (b : ℤ) = m * (7 * m - 5)) →
        f (a + b) = f a + f b) :
    ∀ n : ℕ, f n = n

Sources

Poo-Sung Park, On the Additive Uniqueness of Generalized Nonagonal Numbers for Multiplicative Functions, INTEGERS 25 (2025), Article A99, Theorem 1.

TheoremNonagonal additive uniqueness: the values up to 11#●ready to prove

Let \(f\) be a multiplicative arithmetic function with values in \(\mathbb{C}\) such that \(f(a + b) = f(a) + f(b)\) for all positive integers \(a\) and \(b\) that are generalized nonagonal numbers, that is, \(2a = m(7m - 5)\) and \(2b = k(7k - 5)\) for some integers \(m\) and \(k\). Then \(f(n) = n\) for every integer \(n\) with \(1 \le n \le 11\).

public theorem_wanted multiplicative_nonagonal_additive_eq_self_of_le_eleven
    (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ a b : ℕ, 0 < a → 0 < b →
      (∃ m : ℤ, 2 * (a : ℤ) = m * (7 * m - 5)) → (∃ m : ℤ, 2 * (b : ℤ) = m * (7 * m - 5)) →
        f (a + b) = f a + f b) :
    ∀ n : ℕ, 1 ≤ n → n ≤ 11 → f n = n

Sources

Poo-Sung Park, On the Additive Uniqueness of Generalized Nonagonal Numbers for Multiplicative Functions, INTEGERS 25 (2025), Article A99, Lemma 1.

TheoremNonagonal additive uniqueness: the step at powers of 3#●ready to prove

Let \(f\) be a multiplicative arithmetic function with values in \(\mathbb{C}\) such that \(f(a + b) = f(a) + f(b)\) for all positive integers \(a\) and \(b\) that are generalized nonagonal numbers, that is, \(2a = m(7m - 5)\) and \(2b = k(7k - 5)\) for some integers \(m\) and \(k\). Let \(r\) be a natural number and put \(\alpha(x) = \frac{14}{17} \cdot \frac{2}{3} x - \frac{12}{17}\). If \(f(n) = n\) for every natural number \(n < \alpha(3^r)\), then \(f(3^r) = 3^r\).

public theorem_wanted multiplicative_nonagonal_additive_three_pow
    (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ a b : ℕ, 0 < a → 0 < b →
      (∃ m : ℤ, 2 * (a : ℤ) = m * (7 * m - 5)) → (∃ m : ℤ, 2 * (b : ℤ) = m * (7 * m - 5)) →
        f (a + b) = f a + f b) (r : ℕ)
    (hind : ∀ n : ℕ, (n : ℝ) < 14 / 17 * (2 / 3) * (3 : ℝ) ^ r - 12 / 17 → f n = n) :
    f (3 ^ r) = (3 ^ r : ℕ)

Sources

Poo-Sung Park, On the Additive Uniqueness of Generalized Nonagonal Numbers for Multiplicative Functions, INTEGERS 25 (2025), Article A99, Theorem 2.

TheoremNonagonal additive uniqueness: the step at powers of 5#●ready to prove

Let \(f\) be a multiplicative arithmetic function with values in \(\mathbb{C}\) such that \(f(a + b) = f(a) + f(b)\) for all positive integers \(a\) and \(b\) that are generalized nonagonal numbers, that is, \(2a = m(7m - 5)\) and \(2b = k(7k - 5)\) for some integers \(m\) and \(k\). Let \(r \ge 3\) be a natural number and put \(\beta(x) = x/4\). If \(f(n) = n\) for every natural number \(n \le \beta(5^r)\), then \(f(5^r) = 5^r\).

public theorem_wanted multiplicative_nonagonal_additive_five_pow
    (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ a b : ℕ, 0 < a → 0 < b →
      (∃ m : ℤ, 2 * (a : ℤ) = m * (7 * m - 5)) → (∃ m : ℤ, 2 * (b : ℤ) = m * (7 * m - 5)) →
        f (a + b) = f a + f b) {r : ℕ} (hr : 3 ≤ r)
    (hind : ∀ n : ℕ, (n : ℝ) ≤ (5 : ℝ) ^ r / 4 → f n = n) :
    f (5 ^ r) = (5 ^ r : ℕ)

Sources

Poo-Sung Park, On the Additive Uniqueness of Generalized Nonagonal Numbers for Multiplicative Functions, INTEGERS 25 (2025), Article A99, Theorem 3.

TheoremNonagonal additive uniqueness: the step at powers of 7#●ready to prove

Let \(f\) be a multiplicative arithmetic function with values in \(\mathbb{C}\) such that \(f(a + b) = f(a) + f(b)\) for all positive integers \(a\) and \(b\) that are generalized nonagonal numbers, that is, \(2a = m(7m - 5)\) and \(2b = k(7k - 5)\) for some integers \(m\) and \(k\). Let \(r\) be a natural number. If \(f(n) = n\) for every natural number \(n < 7^r\), then \(f(7^r) = 7^r\).

public theorem_wanted multiplicative_nonagonal_additive_seven_pow
    (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ a b : ℕ, 0 < a → 0 < b →
      (∃ m : ℤ, 2 * (a : ℤ) = m * (7 * m - 5)) → (∃ m : ℤ, 2 * (b : ℤ) = m * (7 * m - 5)) →
        f (a + b) = f a + f b) (r : ℕ)
    (hind : ∀ n : ℕ, n < 7 ^ r → f n = n) :
    f (7 ^ r) = (7 ^ r : ℕ)

Sources

Poo-Sung Park, On the Additive Uniqueness of Generalized Nonagonal Numbers for Multiplicative Functions, INTEGERS 25 (2025), Article A99, Theorem 4.

TheoremNonagonal additive uniqueness: the step at powers of 2#●ready to prove

Let \(f\) be a multiplicative arithmetic function with values in \(\mathbb{C}\) such that \(f(a + b) = f(a) + f(b)\) for all positive integers \(a\) and \(b\) that are generalized nonagonal numbers, that is, \(2a = m(7m - 5)\) and \(2b = k(7k - 5)\) for some integers \(m\) and \(k\). Let \(r\) be a natural number. If \(f(n) = n\) for every natural number \(n < 2^r\), then \(f(2^r) = 2^r\).

public theorem_wanted multiplicative_nonagonal_additive_two_pow
    (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ a b : ℕ, 0 < a → 0 < b →
      (∃ m : ℤ, 2 * (a : ℤ) = m * (7 * m - 5)) → (∃ m : ℤ, 2 * (b : ℤ) = m * (7 * m - 5)) →
        f (a + b) = f a + f b) (r : ℕ)
    (hind : ∀ n : ℕ, n < 2 ^ r → f n = n) :
    f (2 ^ r) = (2 ^ r : ℕ)

Sources

Poo-Sung Park, On the Additive Uniqueness of Generalized Nonagonal Numbers for Multiplicative Functions, INTEGERS 25 (2025), Article A99, Theorem 5.

TheoremParallelogram uniqueness of squares for multiplicative functions#●ready to prove

Let \(f\) be a complex-valued multiplicative arithmetic function (so \(f(0) = 0\)) such that \(f(m^2 + n^2) + f(m^2 - n^2) = 2f(m^2) + 2f(n^2)\) for all integers \(m > n \ge 1\), and suppose \(f(4) \ne 0\). Then \(f(n) = n^2\) for every natural number \(n\).

public theorem_wanted multiplicative_parallelogram_squares_eq_sq (f : ArithmeticFunction ℂ)
    (hf : f.IsMultiplicative)
    (hpar : ∀ m n : ℕ, 0 < n → n < m →
      f (m ^ 2 + n ^ 2) + f (m ^ 2 - n ^ 2) = 2 * f (m ^ 2) + 2 * f (n ^ 2))
    (h4 : f 4 ≠ 0) :
    ∀ n : ℕ, f n = (n : ℂ) ^ 2

Sources

Poo-Sung Park, On the Parallelogram Uniqueness of Square Numbers for Multiplicative Functions, INTEGERS 24 (2024), Article A108, Theorem 1.

TheoremMultiplicative parallelogram solutions vanishing at 4#●ready to prove

Let \(f\) be a complex-valued multiplicative arithmetic function (so \(f(0) = 0\)) such that \(f(m^2 + n^2) + f(m^2 - n^2) = 2f(m^2) + 2f(n^2)\) for all integers \(m > n \ge 1\), and suppose \(f(4) = 0\). Then one of the following holds: (1) for every natural number \(n\), \(f(n) = 0\) if \(n \equiv 0 \pmod 4\), \(f(n) = 4\) if \(n \equiv 2 \pmod 4\), and \(f(n) = 1\) otherwise; (2) \(f(2) = 4\), \(f(2^r) = 0\) for every \(r \ge 2\), and \(f(p^r) = \left(\frac{-1}{p}\right)^r p^r\) for every odd prime \(p\) and every \(r \ge 1\), where \(\left(\frac{-1}{p}\right)\) is the Jacobi symbol.

public theorem_wanted multiplicative_parallelogram_squares_of_f_four_eq_zero
    (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hpar : ∀ m n : ℕ, 0 < n → n < m →
      f (m ^ 2 + n ^ 2) + f (m ^ 2 - n ^ 2) = 2 * f (m ^ 2) + 2 * f (n ^ 2))
    (h4 : f 4 = 0) :
    (∀ n : ℕ, f n = if n % 4 = 0 then 0 else if n % 4 = 2 then 4 else 1) ∨
      (f 2 = 4 ∧ (∀ r : ℕ, 2 ≤ r → f (2 ^ r) = 0) ∧
        ∀ p r : ℕ, p.Prime → p ≠ 2 → 1 ≤ r →
          f (p ^ r) = ((jacobiSym (-1) p : ℤ) : ℂ) ^ r * (p : ℂ) ^ r)

Sources

Poo-Sung Park, On the Parallelogram Uniqueness of Square Numbers for Multiplicative Functions, INTEGERS 24 (2024), Article A108, Theorem 2.

TheoremValues of a parallelogram-equation multiplicative function at powers of two#●ready to prove

Let \(f\) be a complex-valued multiplicative arithmetic function such that \(f(m^2 + n^2) + f(m^2 - n^2) = 2f(m^2) + 2f(n^2)\) for all integers \(m > n \ge 1\). If \(f(4) = 0\), then \(f(2^r) = 0\) for every integer \(r \ge 2\). If \(f(4) \ne 0\), then \(f(2^r) = 2^{2r}\) for every integer \(r \ge 1\).

public theorem_wanted parallelogram_multiplicative_two_pow (f : ArithmeticFunction ℂ)
    (hf : f.IsMultiplicative)
    (hpar : ∀ m n : ℕ, 0 < n → n < m →
      f (m ^ 2 + n ^ 2) + f (m ^ 2 - n ^ 2) = 2 * f (m ^ 2) + 2 * f (n ^ 2)) :
    (f 4 = 0 → ∀ r : ℕ, 2 ≤ r → f (2 ^ r) = 0) ∧
      (f 4 ≠ 0 → ∀ r : ℕ, 1 ≤ r → f (2 ^ r) = (2 : ℂ) ^ (2 * r))

Sources

Poo-Sung Park, On the Parallelogram Uniqueness of Square Numbers for Multiplicative Functions, INTEGERS 24 (2024), Article A108, Theorem 3.

TheoremParallelogram induction: the value at p² + 1#●ready to prove

Let \(f\) be a complex-valued multiplicative arithmetic function (so \(f(0) = 0\)) such that \(f(m^2 + n^2) + f(m^2 - n^2) = 2f(m^2) + 2f(n^2)\) for all integers \(m > n \ge 1\). Let \(p\) be a prime such that \(f(q^s) = q^{2s}\) for every prime \(q < p\) and every integer \(s \ge 1\). If \(p\) is odd and \(f(p) = p^2\), then \(f(p^2 + 1) = (p^2 + 1)^2\).

The hypothesis \(p \ne 2\) is needed: the function with \(f(n) = 0\) if \(4 \mid n\), \(f(n) = 4\) if \(n \equiv 2 \pmod 4\) and \(f(n) = 1\) otherwise satisfies the hypotheses for \(p = 2\), but \(f(5) = 1\).

public theorem_wanted parallelogram_multiplicative_sq_add_one (f : ArithmeticFunction ℂ)
    (hf : f.IsMultiplicative)
    (hpar : ∀ m n : ℕ, 0 < n → n < m →
      f (m ^ 2 + n ^ 2) + f (m ^ 2 - n ^ 2) = 2 * f (m ^ 2) + 2 * f (n ^ 2))
    {p : ℕ} (hp : p.Prime)
    (hind : ∀ q s : ℕ, q.Prime → q < p → 1 ≤ s → f (q ^ s) = (q : ℂ) ^ (2 * s))
    (hp2 : p ≠ 2) (hfp : f p = (p : ℂ) ^ 2) :
    f (p ^ 2 + 1) = ((p ^ 2 + 1 : ℕ) : ℂ) ^ 2

Sources

Poo-Sung Park, On the Parallelogram Uniqueness of Square Numbers for Multiplicative Functions, INTEGERS 24 (2024), Article A108, Lemma 1.

TheoremParallelogram induction: the values at p + 2 and (p + 2)²#●ready to prove

Let \(f\) be a complex-valued multiplicative arithmetic function (so \(f(0) = 0\)) such that \(f(m^2 + n^2) + f(m^2 - n^2) = 2f(m^2) + 2f(n^2)\) for all integers \(m > n \ge 1\). Let \(p\) be a prime such that \(f(q^s) = q^{2s}\) for every prime \(q < p\) and every integer \(s \ge 1\). If \(p \equiv 3 \pmod 4\), then \(f(p + 2) = (p + 2)^2\) and \(f((p + 2)^2) = (p + 2)^4\).

public theorem_wanted parallelogram_multiplicative_add_two (f : ArithmeticFunction ℂ)
    (hf : f.IsMultiplicative)
    (hpar : ∀ m n : ℕ, 0 < n → n < m →
      f (m ^ 2 + n ^ 2) + f (m ^ 2 - n ^ 2) = 2 * f (m ^ 2) + 2 * f (n ^ 2))
    {p : ℕ} (hp : p.Prime)
    (hind : ∀ q s : ℕ, q.Prime → q < p → 1 ≤ s → f (q ^ s) = (q : ℂ) ^ (2 * s))
    (hp4 : p % 4 = 3) :
    f (p + 2) = ((p + 2 : ℕ) : ℂ) ^ 2 ∧ f ((p + 2) ^ 2) = ((p + 2 : ℕ) : ℂ) ^ 4

Sources

Poo-Sung Park, On the Parallelogram Uniqueness of Square Numbers for Multiplicative Functions, INTEGERS 24 (2024), Article A108, Lemma 2.

TheoremParallelogram induction: the values at k² + 1 and 4k² + 1#●ready to prove

Let \(f\) be a complex-valued multiplicative arithmetic function (so \(f(0) = 0\)) such that \(f(m^2 + n^2) + f(m^2 - n^2) = 2f(m^2) + 2f(n^2)\) for all integers \(m > n \ge 1\). Let \(p\) be a prime such that \(f(q^s) = q^{2s}\) for every prime \(q < p\) and every integer \(s \ge 1\). If \(p = 4k - 1\) for a natural number \(k\), then \(f(k^2 + 1) = (k^2 + 1)^2\) and \(f(4k^2 + 1) = (4k^2 + 1)^2\).

public theorem_wanted parallelogram_multiplicative_k_sq_add_one (f : ArithmeticFunction ℂ)
    (hf : f.IsMultiplicative)
    (hpar : ∀ m n : ℕ, 0 < n → n < m →
      f (m ^ 2 + n ^ 2) + f (m ^ 2 - n ^ 2) = 2 * f (m ^ 2) + 2 * f (n ^ 2))
    {p : ℕ} (hp : p.Prime)
    (hind : ∀ q s : ℕ, q.Prime → q < p → 1 ≤ s → f (q ^ s) = (q : ℂ) ^ (2 * s))
    {k : ℕ} (hpk : p = 4 * k - 1) :
    f (k ^ 2 + 1) = ((k ^ 2 + 1 : ℕ) : ℂ) ^ 2 ∧ f (4 * k ^ 2 + 1) = ((4 * k ^ 2 + 1 : ℕ) : ℂ) ^ 2

Sources

Poo-Sung Park, On the Parallelogram Uniqueness of Square Numbers for Multiplicative Functions, INTEGERS 24 (2024), Article A108, Lemma 3.

TheoremParallelogram induction: the value at 5k + 3#●ready to prove

Let \(f\) be a complex-valued multiplicative arithmetic function (so \(f(0) = 0\)) such that \(f(m^2 + n^2) + f(m^2 - n^2) = 2f(m^2) + 2f(n^2)\) for all integers \(m > n \ge 1\). Let \(p\) be a prime such that \(f(q^s) = q^{2s}\) for every prime \(q < p\) and every integer \(s \ge 1\). If \(p = 4k - 1\) for a natural number \(k\) with \(4 \nmid k\), and \(p \ge 19\), then \(f(5k + 3) = (5k + 3)^2\).

public theorem_wanted parallelogram_multiplicative_five_k_add_three (f : ArithmeticFunction ℂ)
    (hf : f.IsMultiplicative)
    (hpar : ∀ m n : ℕ, 0 < n → n < m →
      f (m ^ 2 + n ^ 2) + f (m ^ 2 - n ^ 2) = 2 * f (m ^ 2) + 2 * f (n ^ 2))
    {p : ℕ} (hp : p.Prime)
    (hind : ∀ q s : ℕ, q.Prime → q < p → 1 ≤ s → f (q ^ s) = (q : ℂ) ^ (2 * s))
    {k : ℕ} (hpk : p = 4 * k - 1) (h19 : 19 ≤ p) (hk : ¬ 4 ∣ k) :
    f (5 * k + 3) = ((5 * k + 3 : ℕ) : ℂ) ^ 2

Sources

Poo-Sung Park, On the Parallelogram Uniqueness of Square Numbers for Multiplicative Functions, INTEGERS 24 (2024), Article A108, Lemma 4.

TheoremParallelogram induction: the value at 6k + 1#●ready to prove

Let \(f\) be a complex-valued multiplicative arithmetic function (so \(f(0) = 0\)) such that \(f(m^2 + n^2) + f(m^2 - n^2) = 2f(m^2) + 2f(n^2)\) for all integers \(m > n \ge 1\). Let \(p\) be a prime such that \(f(q^s) = q^{2s}\) for every prime \(q < p\) and every integer \(s \ge 1\). If \(p = 4k - 1\) for a natural number \(k\) with \(k \not\equiv 3 \pmod 4\), and \(p \ge 19\), then \(f(6k + 1) = (6k + 1)^2\).

public theorem_wanted parallelogram_multiplicative_six_k_add_one (f : ArithmeticFunction ℂ)
    (hf : f.IsMultiplicative)
    (hpar : ∀ m n : ℕ, 0 < n → n < m →
      f (m ^ 2 + n ^ 2) + f (m ^ 2 - n ^ 2) = 2 * f (m ^ 2) + 2 * f (n ^ 2))
    {p : ℕ} (hp : p.Prime)
    (hind : ∀ q s : ℕ, q.Prime → q < p → 1 ≤ s → f (q ^ s) = (q : ℂ) ^ (2 * s))
    {k : ℕ} (hpk : p = 4 * k - 1) (h19 : 19 ≤ p) (hk : k % 4 ≠ 3) :
    f (6 * k + 1) = ((6 * k + 1 : ℕ) : ℂ) ^ 2

Sources

Poo-Sung Park, On the Parallelogram Uniqueness of Square Numbers for Multiplicative Functions, INTEGERS 24 (2024), Article A108, Lemma 5.

TheoremParallelogram induction: odd prime powers#●ready to prove

Let \(f\) be a complex-valued multiplicative arithmetic function (so \(f(0) = 0\)) such that \(f(m^2 + n^2) + f(m^2 - n^2) = 2f(m^2) + 2f(n^2)\) for all integers \(m > n \ge 1\). Let \(p\) be a prime such that \(f(q^s) = q^{2s}\) for every prime \(q < p\) and every integer \(s \ge 1\). If \(p\) is odd and \(f(p) = p^2\), then \(f(p^r) = p^{2r}\) for every integer \(r \ge 2\).

The hypothesis \(p \ne 2\) is needed: the function with \(f(n) = 0\) if \(4 \mid n\), \(f(n) = 4\) if \(n \equiv 2 \pmod 4\) and \(f(n) = 1\) otherwise satisfies the hypotheses for \(p = 2\), but \(f(4) = 0\).

public theorem_wanted parallelogram_multiplicative_prime_pow (f : ArithmeticFunction ℂ)
    (hf : f.IsMultiplicative)
    (hpar : ∀ m n : ℕ, 0 < n → n < m →
      f (m ^ 2 + n ^ 2) + f (m ^ 2 - n ^ 2) = 2 * f (m ^ 2) + 2 * f (n ^ 2))
    {p : ℕ} (hp : p.Prime)
    (hind : ∀ q s : ℕ, q.Prime → q < p → 1 ≤ s → f (q ^ s) = (q : ℂ) ^ (2 * s))
    (hp2 : p ≠ 2) (hfp : f p = (p : ℂ) ^ 2) :
    ∀ r : ℕ, 2 ≤ r → f (p ^ r) = (p : ℂ) ^ (2 * r)

Sources

Poo-Sung Park, On the Parallelogram Uniqueness of Square Numbers for Multiplicative Functions, INTEGERS 24 (2024), Article A108, Theorem 4.

TheoremParallelogram induction: primes congruent to 1 mod 4#●ready to prove

Let \(f\) be a complex-valued multiplicative arithmetic function (so \(f(0) = 0\)) such that \(f(m^2 + n^2) + f(m^2 - n^2) = 2f(m^2) + 2f(n^2)\) for all integers \(m > n \ge 1\). Let \(p\) be a prime such that \(f(q^s) = q^{2s}\) for every prime \(q < p\) and every integer \(s \ge 1\). If \(p \equiv 1 \pmod 4\), then \(f(p) = p^2\).

public theorem_wanted parallelogram_multiplicative_prime_one_mod_four (f : ArithmeticFunction ℂ)
    (hf : f.IsMultiplicative)
    (hpar : ∀ m n : ℕ, 0 < n → n < m →
      f (m ^ 2 + n ^ 2) + f (m ^ 2 - n ^ 2) = 2 * f (m ^ 2) + 2 * f (n ^ 2))
    {p : ℕ} (hp : p.Prime)
    (hind : ∀ q s : ℕ, q.Prime → q < p → 1 ≤ s → f (q ^ s) = (q : ℂ) ^ (2 * s))
    (hp4 : p % 4 = 1) :
    f p = (p : ℂ) ^ 2

Sources

Poo-Sung Park, On the Parallelogram Uniqueness of Square Numbers for Multiplicative Functions, INTEGERS 24 (2024), Article A108, Theorem 5.

TheoremParallelogram induction: primes congruent to 3 mod 4 from 19 on#●ready to prove

Let \(f\) be a complex-valued multiplicative arithmetic function (so \(f(0) = 0\)) such that \(f(m^2 + n^2) + f(m^2 - n^2) = 2f(m^2) + 2f(n^2)\) for all integers \(m > n \ge 1\). Let \(p\) be a prime such that \(f(q^s) = q^{2s}\) for every prime \(q < p\) and every integer \(s \ge 1\). If \(p = 4k - 1\) for some natural number \(k\) and \(p \ge 19\), then \(f(p) = p^2\).

public theorem_wanted parallelogram_multiplicative_prime_three_mod_four (f : ArithmeticFunction ℂ)
    (hf : f.IsMultiplicative)
    (hpar : ∀ m n : ℕ, 0 < n → n < m →
      f (m ^ 2 + n ^ 2) + f (m ^ 2 - n ^ 2) = 2 * f (m ^ 2) + 2 * f (n ^ 2))
    {p : ℕ} (hp : p.Prime)
    (hind : ∀ q s : ℕ, q.Prime → q < p → 1 ≤ s → f (q ^ s) = (q : ℂ) ^ (2 * s))
    {k : ℕ} (hpk : p = 4 * k - 1) (h19 : 19 ≤ p) :
    f p = (p : ℂ) ^ 2

Sources

Poo-Sung Park, On the Parallelogram Uniqueness of Square Numbers for Multiplicative Functions, INTEGERS 24 (2024), Article A108, Theorem 6.

TheoremA square–triangular number identity#●ready to prove

Let \(t_v = v(v + 1)/2\) denote the \(v\)-th triangular number. For every natural number \(n \ge 2\), \(n^2 + t_{n-2} = (n - 1)^2 + t_n\).

public theorem_wanted sq_add_triangular_sub_two_eq (n : ℕ) (hn : 2 ≤ n) :
    n ^ 2 + (n - 2) * (n - 2 + 1) / 2 = (n - 1) ^ 2 + n * (n + 1) / 2

Sources

Mingyu Kim and Poo-Sung Park, An Additive Uniqueness Pair of Sets for Multiplicative Functions: Squares and Triangular Numbers, INTEGERS 26 (2026), Article A103, Lemma 1.

TheoremSquare–triangular additivity fixes small squares#●ready to prove

Let \(t_v = v(v + 1)/2\) denote the \(v\)-th triangular number, and let \(f\) be a complex-valued multiplicative arithmetic function with \(f(u^2 + t_v) = f(u^2) + f(t_v)\) for all positive integers \(u\) and \(v\). Let \(N \ge 3\) be an integer such that \(f(n) = n\) for every integer \(n\) with \(1 \le n \le N - 1\). Then \(f(m^2) = m^2\) for every integer \(m\) with \(1 \le m \le N - 2\).

public theorem_wanted multiplicative_sq_triangular_additive_sq
    (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ u v : ℕ, 0 < u → 0 < v →
      f (u ^ 2 + v * (v + 1) / 2) = f (u ^ 2) + f (v * (v + 1) / 2))
    (N : ℕ) (hN : 3 ≤ N) (hlt : ∀ n : ℕ, 1 ≤ n → n ≤ N - 1 → f n = n)
    (m : ℕ) (hm : 1 ≤ m) (hmN : m ≤ N - 2) :
    f (m ^ 2) = m ^ 2

Sources

Mingyu Kim and Poo-Sung Park, An Additive Uniqueness Pair of Sets for Multiplicative Functions: Squares and Triangular Numbers, INTEGERS 26 (2026), Article A103, Lemma 2.

TheoremSquare–triangular additivity fixes odd powers of two#●ready to prove

Let \(t_v = v(v + 1)/2\) denote the \(v\)-th triangular number, and let \(f\) be a complex-valued multiplicative arithmetic function with \(f(u^2 + t_v) = f(u^2) + f(t_v)\) for all positive integers \(u\) and \(v\). Let \(N \ge 4\) be an integer such that \(f(n) = n\) for every integer \(n\) with \(1 \le n \le N - 1\). Then \(f(2^{2k-1}) = 2^{2k-1}\) for every positive integer \(k\) with \(2k \le N - 2\).

public theorem_wanted multiplicative_sq_triangular_additive_two_pow_odd
    (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ u v : ℕ, 0 < u → 0 < v →
      f (u ^ 2 + v * (v + 1) / 2) = f (u ^ 2) + f (v * (v + 1) / 2))
    (N : ℕ) (hN : 4 ≤ N) (hlt : ∀ n : ℕ, 1 ≤ n → n ≤ N - 1 → f n = n)
    (k : ℕ) (hk : 0 < k) (hkN : 2 * k ≤ N - 2) :
    f (2 ^ (2 * k - 1)) = 2 ^ (2 * k - 1)

Sources

Mingyu Kim and Poo-Sung Park, An Additive Uniqueness Pair of Sets for Multiplicative Functions: Squares and Triangular Numbers, INTEGERS 26 (2026), Article A103, Lemma 3.

TheoremSquares and triangular numbers are an additive uniqueness pair#●ready to prove

Let \(t_v = v(v + 1)/2\) denote the \(v\)-th triangular number. If \(f\) is a complex-valued multiplicative arithmetic function with \(f(u^2 + t_v) = f(u^2) + f(t_v)\) for all positive integers \(u\) and \(v\), then \(f(n) = n\) for every natural number \(n\).

public theorem_wanted multiplicative_sq_triangular_additive_eq_id
    (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ u v : ℕ, 0 < u → 0 < v →
      f (u ^ 2 + v * (v + 1) / 2) = f (u ^ 2) + f (v * (v + 1) / 2)) :
    ∀ n : ℕ, f n = n

Sources

Mingyu Kim and Poo-Sung Park, An Additive Uniqueness Pair of Sets for Multiplicative Functions: Squares and Triangular Numbers, INTEGERS 26 (2026), Article A103, Theorem 1.

TheoremDubouis's theorem on sums of nonzero squares#●ready to prove

Let \(m \ge 4\) and let \(n\) be a positive integer. Then \(n\) is a sum of \(m\) squares of positive integers if and only if \(n\) does not lie in the exceptional set \(E_m\), where \(E_4 = \{1, 3, 5, 9, 11, 17, 29, 41\} \cup \{2 \cdot 4^r, 6 \cdot 4^r, 14 \cdot 4^r : r \ge 0\}\), \(E_5 = \{1, 2, 3, 4, 6, 7, 9, 10, 12, 15, 18, 33\}\), and for \(m \ge 6\), \(E_m = \{1, \dots, m - 1\} \cup \{m + 1, m + 2, m + 4, m + 5, m + 7, m + 10, m + 13\}\).

public theorem_wanted sum_nonzero_squares_iff_not_mem_exceptional (m n : ℕ) (hm : 4 ≤ m)
    (hn : 0 < n) :
    (∃ a : Fin m → ℕ, (∀ i, a i ≠ 0) ∧ ∑ i, a i ^ 2 = n) ↔
      n ∉ (if m = 4 then
            ({1, 3, 5, 9, 11, 17, 29, 41} : Set ℕ) ∪
              {n | ∃ r : ℕ, n = 2 * 4 ^ r ∨ n = 6 * 4 ^ r ∨ n = 14 * 4 ^ r}
          else if m = 5 then ({1, 2, 3, 4, 6, 7, 9, 10, 12, 15, 18, 33} : Set ℕ)
          else Set.Ico 1 m ∪
            {m + 1, m + 2, m + 4, m + 5, m + 7, m + 10, m + 13})

Sources

Jewel Mahajan, Multiplicative Functions Additive on Partitions of 2k Nonzero Squares, INTEGERS 26 (2026), Article A121, Lemma 1, quoting Dubouis (1911).

TheoremSums of six and of eight nonzero squares#●ready to prove

Every integer \(n \ge 20\) is a sum of \(6\) squares of positive integers, and every integer \(n \ge 22\) is a sum of \(8\) squares of positive integers.

public theorem_wanted sum_six_and_eight_nonzero_squares :
    (∀ n : ℕ, 20 ≤ n → ∃ a : Fin 6 → ℕ, (∀ i, a i ≠ 0) ∧ ∑ i, a i ^ 2 = n) ∧
      ∀ n : ℕ, 22 ≤ n → ∃ a : Fin 8 → ℕ, (∀ i, a i ≠ 0) ∧ ∑ i, a i ^ 2 = n

Sources

Jewel Mahajan, Multiplicative Functions Additive on Partitions of 2k Nonzero Squares, INTEGERS 26 (2026), Article A121, Corollary 1, as extracted inside the Lemma 1 record.

TheoremSmall values of a multiplicative function 3-additive on sums of two squares#●ready to prove

Let \(E_2 = \{a^2 + b^2 : a, b \ge 1\}\) be the set of sums of two squares of positive integers. If \(f\) is a complex-valued multiplicative function with \(f(2) \ne 0\) such that \(f(A_1 + A_2 + A_3) = f(A_1) + f(A_2) + f(A_3)\) for all \(A_1, A_2, A_3 \in E_2\), then \(f(2) = 2\), \(f(3) = 3\) and \(f(5) = 5\).

public theorem_wanted multiplicative_three_additive_two_squares_base (f : ArithmeticFunction ℂ)
    (hf : f.IsMultiplicative)
    (hadd : ∀ A : Fin 3 → ℕ, (∀ i, ∃ a b : ℕ, 0 < a ∧ 0 < b ∧ A i = a ^ 2 + b ^ 2) →
      f (∑ i, A i) = ∑ i, f (A i))
    (h2 : f 2 ≠ 0) :
    f 2 = 2 ∧ f 3 = 3 ∧ f 5 = 5

Sources

Jewel Mahajan, Multiplicative Functions Additive on Partitions of 2k Nonzero Squares, INTEGERS 26 (2026), Article A121, Lemma 2.

TheoremSmall values of a multiplicative function 4-additive on sums of two squares#●ready to prove

Let \(E_2 = \{a^2 + b^2 : a, b \ge 1\}\) be the set of sums of two squares of positive integers. If \(f\) is a complex-valued multiplicative function with \(f(2) \ne 0\) such that \(f(A_1 + A_2 + A_3 + A_4) = f(A_1) + f(A_2) + f(A_3) + f(A_4)\) for all \(A_1, \dots, A_4 \in E_2\), then \(f(n) = n\) for every \(n \in \{2, 3, 4, 5, 6, 7, 8, 10\}\).

public theorem_wanted multiplicative_four_additive_two_squares_base (f : ArithmeticFunction ℂ)
    (hf : f.IsMultiplicative)
    (hadd : ∀ A : Fin 4 → ℕ, (∀ i, ∃ a b : ℕ, 0 < a ∧ 0 < b ∧ A i = a ^ 2 + b ^ 2) →
      f (∑ i, A i) = ∑ i, f (A i))
    (h2 : f 2 ≠ 0) :
    ∀ n ∈ ({2, 3, 4, 5, 6, 7, 8, 10} : Finset ℕ), f n = n

Sources

Jewel Mahajan, Multiplicative Functions Additive on Partitions of 2k Nonzero Squares, INTEGERS 26 (2026), Article A121, Lemma 3.

TheoremMultiplicative functions additive on six or eight paired squares and nonzero at \(2\) are the identity#●ready to prove

Multiplicative functions additive on six or eight paired squares and nonzero at \(2\) are the identity. Let \(k \in \{3, 4\}\) and let \(f\) be a complex-valued multiplicative function with \(f(2) \ne 0\) such that

\[f\Big(\sum_{j=1}^{k} (x_j^2 + y_j^2)\Big) = \sum_{j=1}^{k} f(x_j^2 + y_j^2)\]

for all positive integers \(x_1, \dots, x_k, y_1, \dots, y_k\). Then \(f(n) = n\) for every positive integer \(n\).

public theorem_wanted multiplicative_additive_paired_squares_eq_id_of_three_or_four
    (k : ℕ) (hk : k = 3 ∨ k = 4) (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ x y : Fin k → ℕ, (∀ j, 0 < x j) → (∀ j, 0 < y j) →
      f (∑ j, (x j ^ 2 + y j ^ 2)) = ∑ j, f (x j ^ 2 + y j ^ 2))
    (h2 : f 2 ≠ 0) :
    ∀ n : ℕ, 0 < n → f n = n

Sources

Jewel Mahajan, Multiplicative Functions Additive on Partitions of 2k Nonzero Squares, INTEGERS 26 (2026), Article A121, Theorem 1.

TheoremDichotomy for multiplicative functions additive on paired squares#●ready to prove

Let \(k \ge 5\) and let \(f\) be a complex-valued multiplicative function such that

\[f\Big(\sum_{j=1}^{k} (x_j^2 + y_j^2)\Big) = \sum_{j=1}^{k} f(x_j^2 + y_j^2)\]

for all positive integers \(x_1, \dots, x_k, y_1, \dots, y_k\). Then either \(f(n) = n\) for every positive integer \(n\), or \(f(n) = 0\) for every positive integer \(n\) that is of the form \(a^2 + b^2\) with integers \(a, b \ge 1\), or of the form \(2k + t\) with \(t \in \{0, 3, 6, 8, 9, 11, 12\}\), or satisfies \(n \ge 2k + 14\).

public theorem_wanted multiplicative_additive_paired_squares_dichotomy
    (k : ℕ) (hk : 5 ≤ k) (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ x y : Fin k → ℕ, (∀ j, 0 < x j) → (∀ j, 0 < y j) →
      f (∑ j, (x j ^ 2 + y j ^ 2)) = ∑ j, f (x j ^ 2 + y j ^ 2)) :
    (∀ n : ℕ, 0 < n → f n = n) ∨
      ∀ n : ℕ, ((∃ a b : ℕ, 0 < a ∧ 0 < b ∧ n = a ^ 2 + b ^ 2) ∨
          (∃ t ∈ ({0, 3, 6, 8, 9, 11, 12} : Finset ℕ), n = 2 * k + t) ∨ 2 * k + 14 ≤ n) →
        f n = 0

Sources

Jewel Mahajan, Multiplicative Functions Additive on Partitions of 2k Nonzero Squares, INTEGERS 26 (2026), Article A121, Theorem 2.

TheoremA nonzero value in the vanishing range of the dichotomy forces the identity#●ready to prove

Let \(k \ge 5\) and let \(f\) be a complex-valued multiplicative function such that

\[f\Big(\sum_{j=1}^{k} (x_j^2 + y_j^2)\Big) = \sum_{j=1}^{k} f(x_j^2 + y_j^2)\]

for all positive integers \(x_1, \dots, x_k, y_1, \dots, y_k\). Suppose that \(f(\beta) \ne 0\) for some positive integer \(\beta\) that is of the form \(a^2 + b^2\) with integers \(a, b \ge 1\), or of the form \(2k + t\) with \(t \in \{0, 3, 6, 8, 9, 11, 12\}\), or satisfies \(\beta \ge 2k + 14\). Then \(f(n) = n\) for every positive integer \(n\).

public theorem_wanted multiplicative_additive_paired_squares_eq_id_of_ne_zero
    (k : ℕ) (hk : 5 ≤ k) (f : ArithmeticFunction ℂ) (hf : f.IsMultiplicative)
    (hadd : ∀ x y : Fin k → ℕ, (∀ j, 0 < x j) → (∀ j, 0 < y j) →
      f (∑ j, (x j ^ 2 + y j ^ 2)) = ∑ j, f (x j ^ 2 + y j ^ 2))
    (β : ℕ) (hβ : (∃ a b : ℕ, 0 < a ∧ 0 < b ∧ β = a ^ 2 + b ^ 2) ∨
      (∃ t ∈ ({0, 3, 6, 8, 9, 11, 12} : Finset ℕ), β = 2 * k + t) ∨ 2 * k + 14 ≤ β)
    (hfβ : f β ≠ 0) :
    ∀ n : ℕ, 0 < n → f n = n

Sources

Jewel Mahajan, Multiplicative Functions Additive on Partitions of 2k Nonzero Squares, INTEGERS 26 (2026), Article A121, Corollary 2.

TheoremMultiplicative functions additive on six paired squares and nonzero at \(2\) are the identity#●ready to prove

Multiplicative functions additive on six paired squares and nonzero at \(2\) are the identity. Let \(f\) be a complex-valued multiplicative function with \(f(2) \ne 0\) such that

\[f\Big(\sum_{j=1}^{3} (x_j^2 + y_j^2)\Big) = \sum_{j=1}^{3} f(x_j^2 + y_j^2)\]

for all positive integers \(x_1, x_2, x_3, y_1, y_2, y_3\). Then \(f(n) = n\) for every positive integer \(n\).

public theorem_wanted multiplicative_additive_six_squares_eq_id (f : ArithmeticFunction ℂ)
    (hf : f.IsMultiplicative)
    (hadd : ∀ x y : Fin 3 → ℕ, (∀ j, 0 < x j) → (∀ j, 0 < y j) →
      f (∑ j, (x j ^ 2 + y j ^ 2)) = ∑ j, f (x j ^ 2 + y j ^ 2))
    (h2 : f 2 ≠ 0) :
    ∀ n : ℕ, 0 < n → f n = n

Sources

Jewel Mahajan, Multiplicative Functions Additive on Partitions of 2k Nonzero Squares, INTEGERS 26 (2026), Article A121, Theorem 3.

TheoremMultiplicative functions additive on eight paired squares and nonzero at \(2\) are the identity#●ready to prove

Multiplicative functions additive on eight paired squares and nonzero at \(2\) are the identity. Let \(f\) be a complex-valued multiplicative function with \(f(2) \ne 0\) such that

\[f\Big(\sum_{j=1}^{4} (x_j^2 + y_j^2)\Big) = \sum_{j=1}^{4} f(x_j^2 + y_j^2)\]

for all positive integers \(x_1, \dots, x_4, y_1, \dots, y_4\). Then \(f(n) = n\) for every positive integer \(n\).

public theorem_wanted multiplicative_additive_eight_squares_eq_id (f : ArithmeticFunction ℂ)
    (hf : f.IsMultiplicative)
    (hadd : ∀ x y : Fin 4 → ℕ, (∀ j, 0 < x j) → (∀ j, 0 < y j) →
      f (∑ j, (x j ^ 2 + y j ^ 2)) = ∑ j, f (x j ^ 2 + y j ^ 2))
    (h2 : f 2 ≠ 0) :
    ∀ n : ℕ, 0 < n → f n = n

Sources

Jewel Mahajan, Multiplicative Functions Additive on Partitions of 2k Nonzero Squares, INTEGERS 26 (2026), Article A121, Theorem 4.

1 fully proved37 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.