Abstract

This entry defines the sum-of-squares r_k(n) function, which counts the number of ways to write a natural number as a sum of squares of integers. Signs and permutations of these integers are taken into account, such that e.g. 1² + 2², 2² + 1², and (-1)² + 2² are all different decompositions of 5.

Using this, I then formalise the main result: Jacobi’s two-square theorem, which states that for n > 0 we have r_2(n) = 4(d_1(n) – d_3(n)) where d_i(n) denotes the number of divisors m of n such that m = i (mod 4).

Corollaries include the identities r_2(2n) = r_2(n) and r_2(p²n) = r_2(n) if p = 3 (mod 4) and the well-known theorem that r_2(n) = 0 iff n has a prime factor p of odd multiplicity with p = 3 (mod 4).

BibTeX

@article{Sum_Of_Squares_Count-AFP,
  author  = {Manuel Eberl},
  title   = {The Sum-of-Squares Function and {J}acobi's Two-Square Theorem},
  journal = {Archive of Formal Proofs},
  month   = {November},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/Sum_Of_Squares_Count.html},
             Formal proof development},
  ISSN    = {2150-914x},
}