Theorem 5.7.1 — The prime-factor criterion for two integer squares

Read-back model: unavailable (the exact runtime model identifier is not exposed).

For every natural number $n$ with $0<n$, there exist integers $x$ and $y$ such that $n=x^2+y^2$, with $n$ interpreted as an integer in this equality, if and only if the following holds: for every natural number $p$, if $p$ is prime, $p$ divides $n$ in the natural numbers, and the remainder of $p$ on division by $4$ is $3$, then the natural number $n.\mathrm{factorization}(p)$ is even. Here $p\mid n$ means that $n=pm$ for some $m\in\mathbb N$; a prime natural number is at least $2$ and has only $1$ and itself as natural divisors. The function $n.\mathrm{factorization}$ is the finitely supported function from natural numbers to natural numbers whose value at a prime $p$, for positive $n$, is the exponent of $p$ in the prime factorization of $n$, equivalently the largest $e\in\mathbb N$ for which $p^e\mid n$; it is $0$ at nonprimes and primes not dividing $n$, and the library defines the entire factorization function of $0$ and of $1$ to be $0$. Evenness means that this exponent equals $r+r$ for some $r\in\mathbb N$. The hypothesis excludes $n=0$ but includes $n=1$, for which the condition on prime divisors is vacuous; more generally that condition is vacuous whenever no prime divisor of $n$ has remainder $3$ modulo $4$. The integers $x,y$ may be zero or negative, and there are no coprimality, distinctness, nonzero, or uniqueness conditions and no further assumptions.