From individual representations to an arithmetic criterion

Writing a positive integer as a sum of two squares is an elementary question with a precise general answer. Some integers have such a representation and others do not; checking a few small inputs does not explain the distinction. A criterion expressed through prime factorization instead decides the question for every positive integer. This project follows Section 5.7 of William Stein's Elementary Number Theory: Primes, Congruences, and Secrets, including the section's supporting statements and one subsequent exercise. The selected material connects divisibility, coprimality, algebraic identities, and rational approximation within a single classical topic. The source is the author-hosted January 2017 text, using its numbering rather than the numbering of earlier drafts.

Integers, representations, and prime exponents

A two-square representation of an integer $n$ consists of integers $x,y$ satisfying $n=x^2+y^2$. Either coordinate may be zero or negative. A representation is primitive when the greatest common divisor of its coordinates is one; this restricts representations, not the definition of representability itself. For a positive integer $n$ and a prime $p$, the prime exponent $v_p(n)$ is the exponent of $p$ in the prime factorization of $n$. The congruence $p\equiv3\pmod4$ means that division of $p$ by four leaves remainder three.

The approximation statement uses a real number $t$, a positive integer $N$, and a reduced fraction $a/b$, where $a$ is an integer, $b$ is a positive integer, and their greatest common divisor is one. These conventions agree with Stein's section and its definition of primitive representations.

Formalization targets

The supporting targets retain their complete source statements. Lemma 5.7.4 concerns every positive integer $n$ with a prime divisor $p\equiv3\pmod4$:

$$\nexists x,y\in\mathbb Z:\quad n=x^2+y^2\quad\text{and}\quad\gcd(x,y)=1.$$

Equation (5.7.1) is the integer identity

$$(x_1^2+y_1^2)(x_2^2+y_2^2)=(x_1x_2-y_1y_2)^2+(x_1y_2+x_2y_1)^2.$$

Lemma 5.7.5 states that, for every real $t$ and positive integer $N$, some reduced fraction satisfies

$$0<b\le N,\qquad |t-a/b|\le\frac{1}{b(N+1)}.$$

The capstone, Theorem 5.7.1, is the complete equivalence

$$n=x^2+y^2\text{ for some }x,y\in\mathbb Z \quad\Longleftrightarrow\quad \forall\text{ primes }p\mid n,\quad p\equiv3\pmod4\Longrightarrow v_p(n)\text{ is even},$$

for every positive integer $n$. Both implications are required. These four statements are located on printed pages 117–120 of the source PDF.

Exercise 5.11, on printed page 122, is an optional downstream target:

$$\forall n\in\mathbb Z,\ \exists k\in\{0,1,2,3\}:\quad \nexists x,y\in\mathbb Z,\ n+k=x^2+y^2.$$

It describes gaps among represented integers and is not a prerequisite milestone for the capstone.

What the criterion and its formalization provide

The criterion replaces a search for coordinates with a finite condition on the factorization of an input. It applies to composite integers as well as primes and distinguishes the exponent of a prime divisor from the mere presence of that divisor. The primitive obstruction also explains why a claim about coprime coordinates must not be confused with a claim that excludes all representations. The composition identity supplies an explicit statement of multiplicative closure, while the exercise gives a uniform restriction on consecutive runs. These are the consequences and accompanying results presented in Stein's treatment.

The mathematics is established, not an open research problem. Important formal ingredients already exist in Mathlib: the sum-of-two-squares development includes the arithmetic criterion and primitive obstruction, and the Diophantine approximation development supplies the bounded-denominator result. The work here is a source-aligned collection of exact theorem interfaces and independently checked proofs. Reusing those results does not claim a new proof of the classical mathematics or an exact transcription of Stein's argument.

Why the complete statement matters

A finite list of successful representations cannot establish an assertion about every positive integer. Similarly, a restriction on primitive representations is insufficient to settle general representability, because a nonprimitive pair is still a valid representation. The capstone must account for prime exponents and both directions of the equivalence simultaneously. The approximation result has its own coupled requirements: obtaining a small denominator without the stated error bound, or a good approximation with an uncontrolled denominator, does not meet the target. These distinctions are explicit in the source statements.

Formalization scope

The namespace is SteinENT. Inputs $n,p,N$ use natural numbers, with positivity hypotheses wherever the source uses positive integers. Coordinates and all subtraction in the composition identity use integers. Prime exponents use Nat.factorization; primitivity uses Int.gcd x y = 1. Approximation witnesses use Lean's rational type, whose canonical numerator and positive denominator already express a reduced fraction. The error inequality is an inequality of real numbers. The gap exercise allows every integer starting point, including negative ones.

No hypothesis assumes the desired representation or restricts the capstone to a bounded test range. There is no additional definition that hides a proof obligation, and no separate alias item for primitivity. Standard Mathlib arithmetic, rational approximation, and tactic libraries provide reusable infrastructure. Complete alternative proofs are welcome when they preserve these interfaces, including the explicit positive-input boundary and unrestricted integer coordinates.

Selected references

• William Stein, Elementary Number Theory: Primes, Congruences, and Secrets, Undergraduate Texts in Mathematics, Springer, 2008; author-hosted January 2017 version, Section 5.7 and Exercise 5.11. Author's book page.
• William Stein, author's source text at commit c4984c7ddb22258674816f8c000b0d8eb485d694, corresponding section and exercises.
• The Mathlib Community, Mathlib4 at commit 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e, Lean 4 library, pinned formalization environment; number-theory modules linked above.