Sums of three squares

TheoremLegendre's three-square theorem#✓fully proved

Every natural number \(n\) that is not of the form \(4^a (8b + 7)\) with natural numbers \(a, b\) is a sum of three squares: there are natural numbers \(x, y, z\) with \(x^2 + y^2 + z^2 = n\).

theorem exists_three_squares_of_not_four_pow_mul_eight_mul_add_seven
    (n : Nat)
    (h : ¬ ∃ a b : Nat, n = 4 ^ a * (8 * b + 7)) :
    ∃ x y z : Nat, x ^ 2 + y ^ 2 + z ^ 2 = n
Sources
  • Soufiane Mezroui, Abdelmalek Azizi, and M'hammed Ziane, "On a Conjecture of Farhi", Journal of Integer Sequences 17 (2014), source TeX lines 122-127, https://cs.uwaterloo.ca/journals/JIS/VOL17/Mezroui/soufiane4.tex.
Used by 3
Used bySums of three terms of the sequence ⌊n²/8⌋ · Gauss's Eureka theorem · Cauchy's lemma

TheoremConverse of Legendre's three-square theorem#✓fully proved

If a natural number \(n\) is a sum of three squares of natural numbers, then \(n\) is not of the form \(4^a (8b + 7)\) with natural numbers \(a, b\).

theorem not_exists_four_pow_mul_eight_mul_add_seven_of_exists_three_squares
    (n : Nat)
    (h : ∃ x y z : Nat, x ^ 2 + y ^ 2 + z ^ 2 = n) :
    ¬ ∃ a b : Nat, n = 4 ^ a * (8 * b + 7)
Sources
  • Fabián Arias, Jerson Borja, and Luis Rubio, "Counting Integers Representable as Images of Polynomials Modulo n", Journal of Integer Sequences 22 (2019), Article 19.6.7, theorem, lines 134–136, https://cs.uwaterloo.ca/journals/JIS/VOL22/Borja/borja3.tex.

TheoremSums of three terms of the sequence ⌊n²/8⌋#✓fully proved

For every natural number \(m\) there are natural numbers \(a\), \(b\), \(c\) with \(m = \lfloor a^2/8 \rfloor + \lfloor b^2/8 \rfloor + \lfloor c^2/8 \rfloor\).

public theorem every_nat_eq_sum_three_sq_div_eight (m : ℕ) :
    ∃ a b c : ℕ, m = a ^ 2 / 8 + b ^ 2 / 8 + c ^ 2 / 8
Sources
Uses 1
Proof usesLegendre's three-square theorem

DefinitionNumber of representations as a sum of three squares#✓fully proved

For a natural number \(n\), \(r_3(n)\) is the number of ordered triples \((x, y, z)\) of integers in the interval \([-n, n]\) with \(x^2 + y^2 + z^2 = n\). Every integer solution of \(x^2 + y^2 + z^2 = n\) lies in this interval (also for \(n = 0\)), so \(r_3(n)\) is the number of all ordered integer solutions.

def threeSquareRepresentationCount (n : ℕ) : ℕ :=
  ((((Finset.Icc (-(n : ℤ)) (n : ℤ)) ×ˢ (Finset.Icc (-(n : ℤ)) (n : ℤ))) ×ˢ
      (Finset.Icc (-(n : ℤ)) (n : ℤ))).filter
      (fun p : (ℤ × ℤ) × ℤ => p.1.1 ^ 2 + p.1.2 ^ 2 + p.2 ^ 2 = (n : ℤ))).card
Sources
  • Primary source: E. T. Mortenson, arXiv:1702.01627v2, Mortenson-AC-Gauss-arxiv-v2.tex lines 127-131 defining rₛ by Rₛ(q) = ∑ₙ rₛ(n) (-q) ^ n = (∑_{m ∈ ℤ} (-1) ^ m q ^ (m ^ 2)) ^ s (ordered signed integer tuples). Ranked source arXiv:2307.05244 main.tex lines 78-82 identifies the equation x ^ 2 + y ^ 2 + z ^ 2 = n.
Used by 8
Used byOverpartitions of \(5n\) modulo \(5\) · The three-square count counts all integer solutions · Gauss's three-square formula after Aygin and Williams · Legendre-symbol recursion for three-square counts · Removing a factor of 4 preserves the three-square count · Gauss's three-square formula, residues 1, 2, 5, 6 modulo 8 · Gauss's three-square formula, residue 3 modulo 8 · Numbers congruent to 7 modulo 8 are not sums of three squares

TheoremNumbers congruent to 7 modulo 8 are not sums of three squares#✓fully proved

For a natural number \(m\), let \(r_3(m)\) denote the number of ordered triples of integers \((x, y, z)\) with \(x^2 + y^2 + z^2 = m\). For every positive natural number \(n\) with \(n \equiv 7 \pmod 8\), \(r_3(n) = 0\). This is the case \(n \equiv 7 \pmod 8\) of Gauss's formula for \(r_3\).

theorem threeSquareRepresentationCount_eq_zero_of_mod_eight_eq_seven
    (n : ℕ) (hn : 0 < n) (h : n % 8 = 7) :
    threeSquareRepresentationCount n = 0
Sources
  • arXiv:2307.05244 main.tex lines 191-199.
Uses 1
Statement usesNumber of representations as a sum of three squares

TheoremRemoving a factor of 4 preserves the three-square count#✓fully proved

For a natural number \(m\), let \(r_3(m)\) denote the number of ordered triples of integers \((x, y, z)\) with \(x^2 + y^2 + z^2 = m\). For every positive natural number \(n\) divisible by \(4\), \(r_3(n) = r_3(n/4)\). This is the case \(4 \mid n\) of Gauss's formula for \(r_3\).

theorem threeSquareRepresentationCount_eq_threeSquareRepresentationCount_div_four
    (n : ℕ) (hn : 0 < n) (h : n % 4 = 0) :
    threeSquareRepresentationCount n = threeSquareRepresentationCount (n / 4)
Sources
  • arXiv:2307.05244 main.tex lines 191-199.
Uses 1
Statement usesNumber of representations as a sum of three squares

TheoremLegendre-symbol recursion for three-square counts#✓fully proved

For a natural number \(m\), let \(r_3(m)\) denote the number of ordered triples of integers \((x, y, z)\) with \(x^2 + y^2 + z^2 = m\). Let \(p \ge 3\) be a prime and let \(n \ge 1\) and \(\alpha \ge 0\) be natural numbers. Then

\[ r_3(p^{2\alpha} n) = \left(\frac{p^{\alpha+1} - 1}{p - 1} - \left(\frac{-n}{p}\right) \frac{p^{\alpha} - 1}{p - 1}\right) r_3(n) - p \, \frac{p^{\alpha} - 1}{p - 1} \, r_3(n/p^2), \]

where \(\left(\frac{-n}{p}\right)\) is the Legendre symbol, both quotients by \(p - 1\) are exact integer divisions, and the term \(r_3(n/p^2)\) is read as \(0\) when \(p^2\) does not divide \(n\).

Proof: The route is an elementary p-neighbour double count using quaternionic descent and finite-field conic counts, followed by a two-step induction on the exponent.

public theorem r3_legendre_recursion
    {p n α : ℕ} [Fact (Nat.Prime p)] (hp3 : 3 ≤ p) (hn : 1 ≤ n) :
    (Nat.threeSquareRepresentationCount (p ^ (2 * α) * n) : ℤ) =
      (((((p : ℤ) ^ (α + 1) - 1) / ((p : ℤ) - 1)) -
          legendreSym p (-(n : ℤ)) *
            (((p : ℤ) ^ α - 1) / ((p : ℤ) - 1))) *
          Nat.threeSquareRepresentationCount n -
        (p : ℤ) * (((p : ℤ) ^ α - 1) / ((p : ℤ) - 1)) *
          (if p ^ 2 ∣ n then Nat.threeSquareRepresentationCount (n / p ^ 2) else 0))
Sources
Uses 1
Statement usesNumber of representations as a sum of three squares

DefinitionHurwitz class number#●ready to state

The Hurwitz class number is the function \(H\) from the natural numbers to the rationals given by \(H(0) = -1/12\); \(H(N) = 0\) if \(N \equiv 1\) or \(2 \pmod 4\); and, for \(N > 0\) with \(N \equiv 0\) or \(3 \pmod 4\), \(H(N)\) is the number of equivalence classes of positive-definite integral binary quadratic forms of discriminant \(-N\), primitive or not, where the class of a form equivalent to \(a (x^2 + y^2)\) for some positive integer \(a\) counts with weight \(1/2\), the class of a form equivalent to \(a (x^2 + x y + y^2)\) for some positive integer \(a\) counts with weight \(1/3\), and every other class counts with weight \(1\).

def_wanted hurwitzClassNumber : ℕ → ℚ
Sources
  • arXiv:2307.05244 main.tex lines 359-365: H(N) = 0 if N ≡ 1 or 2 mod 4; H(0) = -1 / 12; otherwise N > 0 and N ≡ 0 or 3 mod 4, H(N) is the class number of not necessarily primitive positive-definite quadratic forms of discriminant -N, with weight 1 / 2 for forms equivalent to a * (x ^ 2 + y ^ 2) and weight 1 / 3 for forms equivalent to a * (x ^ 2 + x * y + y ^ 2).
Used by 2
Used byGauss's three-square formula, residues 1, 2, 5, 6 modulo 8 · Gauss's three-square formula, residue 3 modulo 8

TheoremGauss's three-square formula, residues 1, 2, 5, 6 modulo 8#●statement formalized

For every positive natural number \(n\) with \(n \equiv 1\), \(2\), \(5\) or \(6 \pmod 8\), the number \(r_3(n)\) of ordered triples \((x, y, z)\) of integers with \(x^2 + y^2 + z^2 = n\) equals \(12 H(4n)\), where \(H\) is the Hurwitz class number.

theorem_wanted threeSquareRepresentationCount_eq_twelve_mul_hurwitzClassNumber_four_n
    (n : ℕ) (hn : 0 < n)
    (h : n % 8 = 1 ∨ n % 8 = 2 ∨ n % 8 = 5 ∨ n % 8 = 6) :
    (threeSquareRepresentationCount n : ℚ) = 12 * ❰hurwitzClassNumber❱ (4 * n)
Sources
  • arXiv:2307.05244 main.tex lines 191-199.
Uses 2
Statement usesHurwitz class number · Number of representations as a sum of three squares

TheoremGauss's three-square formula, residue 3 modulo 8#●statement formalized

For every positive natural number \(n\) with \(n \equiv 3 \pmod 8\), the number \(r_3(n)\) of ordered triples \((x, y, z)\) of integers with \(x^2 + y^2 + z^2 = n\) equals \(24 H(n)\), where \(H\) is the Hurwitz class number.

theorem_wanted threeSquareRepresentationCount_eq_twenty_four_mul_hurwitzClassNumber
    (n : ℕ) (hn : 0 < n) (h : n % 8 = 3) :
    (threeSquareRepresentationCount n : ℚ) = 24 * ❰hurwitzClassNumber❱ n
Sources
  • arXiv:2307.05244 main.tex lines 191-199.
Uses 2
Statement usesHurwitz class number · Number of representations as a sum of three squares
7 fully proved2 statement formalized1 ready to state

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.