TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Characterisation of primitive sums of two squares

Statement

A positive integer $n$ has a primitive two-square representation if and only if $v_{2} (n) \leq 1$ and no prime $q \equiv 3 (m o d 4)$ divides $n$ .

Facts & Assumptions

Given: A positive integer $n$ .

[F1]

A two-square representation is primitive when its coordinate gcd is $1$ (Representations and primitive representations as sums of two squares).

[L1]

If $q \equiv 3 (m o d 4)$ is prime and $q ∣ x^{2} + y^{2}$ , then $q ∣ x$ and $q ∣ y$ (A prime congruent to $3$ modulo $4$ divides both coordinates of a divisible two-square sum).

[L2]

If $P = a^{2} + b^{2}$ and $Q = c^{2} + d^{2}$ are primitive representations with $\gcd (P, Q) = 1$ , then the Brahmagupta–Fibonacci construction gives a primitive representation of $P Q$ (Coprime primitively represented factors have a primitive product representation).

[L3]

Every natural power of a prime congruent to $1$ modulo $4$ has a primitive two-square representation (Powers of primes congruent to $1$ modulo $4$ have primitive two-square representations).

[L4]

A positive integer is the finite product of the powers of its prime divisors with their canonical valuations (For $n \geq 1$ and any injective list $p : r \to Z$ of primes containing every prime divisor of $n$ , one has $n = \prod_{i < r} p_{i}^{v_{p_{i}} (n)}$ ; the exponents are determined by $n$ , and $v_{q} (n) = 0$ for every prime $q$ outside the list).

[L5]

For a prime $p$ and a nonzero integer $n$ , and every $k \in N$ : $p^{k} ∣ n$ if and only if $k \leq v_{p} (n)$ ; in particular $v_{p} (n) \geq 1$ if and only if $p ∣ n$ (For a prime $p$ and a nonzero integer $a$ : $p^{v_{p} (a)} ∣ a$ and $p^{v_{p} (a) + 1} ∤ a$ ; $p^{k} ∣ a$ holds exactly for $k \leq v_{p} (a)$ ; $v_{p} (a) \geq 1$ exactly when $p ∣ a$ ; $v_{p} (1) = v_{p} (- 1) = 0$ ; and $v_{p} (p) = 1$ ).

[L6]

For a finite pairwise-coprime list with partial products $P_{k}$ , one has $\gcd (P_{k}, n_{j}) = 1$ whenever $k \leq j$ (For a finite pairwise-coprime list of positive integers, the product divides every common multiple, and each initial product is coprime to every remaining modulus).

[L7]

If a prime $p$ divides $a b$ , then $p ∣ a$ or $p ∣ b$ (Euclid's lemma: if $p$ is prime and $p ∣ a b$ then $p ∣ a$ or $p ∣ b$ ).

[L8]

If a property holds at $0$ and passes from $j$ to $j + 1$ , it holds for every $j \in N$ (The principle of mathematical induction).

Proof

technique · direct

1.1givenF1L1

For the forward direction, if $n = x^{2} + y^{2}$ primitively and a prime $q \equiv 3 (m o d 4)$ divided $n$ , [L1] would make $q$ divide both coordinates, contrary to [F1].

1.2F1L5algebra

Squares modulo $4$ show that $4 ∣ x^{2} + y^{2}$ forces both $x$ and $y$ even. Thus a primitive representation has $4 ∤ n$ , and the divisibility clause of [L5] at $p = 2$ , $k = 2$ makes that equivalent to $v_{2} (n) \leq 1$ .

1.3givenL4L5L7algebra

For the reverse direction, assume the two stated prime conditions. In [L4], no three-mod-four prime occurs, the factor $2$ occurs with exponent at most one, and all remaining nontrivial factors are powers of distinct primes congruent to one modulo four. The factors are pairwise coprime by uniqueness and [L7].

2.1step 1.3L3F1construct

The possible factor $2$ has the primitive representation $(1, 1)$ , and every one-mod-four prime power has a primitive representation by [L3].

3.1step 1.3step 2.1L2L6L8F1discharge-induction

Combine these pairwise-coprime primitive representations one at a time using [L2]. The partial product is coprime to the next factor by [L6], so [L8] completes the finite induction. If the factor list is empty, $n = 1$ and $(1, 0)$ is primitive.

4.1step 1.1step 1.2step 3.1∎

Steps 1.1 and 1.2 prove necessity, while step 3.1 proves sufficiency.

Depends on

Used by

Dependency tree · two levels

50 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

P. Hackman, Elementary Number Theory, Chapter E, Theorem E.II.4 and Lemmas E.II.5–E.II.6 (standard reference, not scraped)