CorollaryStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

Squarefree sums of two squares

Statement

A squarefree positive integer is a sum of two squares if and only if none of its odd prime factors is congruent to $3$ modulo $4$ ; every such representation is primitive.

Facts & Assumptions

Given: A squarefree positive integer $n$ .

[F1]

A positive integer $n$ is squarefree if no square of a prime divides $n$ ; equivalently, every exponent in its canonical prime factorisation is $0$ or $1$ (Squarefree positive integers).

[L1]

A positive integer $n$ is a sum of two squares if and only if every prime $q \equiv 3 (m o d 4)$ occurs to an even exponent in its canonical prime factorisation (Characterisation of positive integers that are sums of two squares).

[L2]

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$ (Characterisation of primitive sums of two squares).

[F2]

An integer $d$ is a common divisor of $a$ and $b$ when $d ∣ a$ and $d ∣ b$ (Common divisor, and the greatest common divisor $\gcd (a, b)$ , with the convention $\gcd (0, 0) : = 0$ ).

[L3]

Every integer greater than $1$ has a prime divisor (Every integer $n > 1$ has a prime divisor; indeed the least divisor of $n$ that exceeds $1$ is prime).

[L4]

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$ ).

Proof

technique · direct

1.1

By [F1], every prime exponent of $n$ is zero or one. Consequently the even-exponent condition in [L1] for a prime congruent to three modulo four is equivalent to that prime not dividing $n$ .

F1L1algebra

1.2

To see that every representation is primitive, suppose $n = x^{2} + y^{2}$ and $\gcd (x, y) > 1$ . By [L3] choose a prime $ℓ$ dividing the gcd. Then $ℓ ∣ x$ and $ℓ ∣ y$ by [F2], so $ℓ^{2} ∣ n$ , contradicting [F1].

F1F2L3L4assume-contraalgebradischarge-contradiction

2.1

Squarefreeness also gives $v_{2} (n) \leq 1$ , so the same exclusion of three-mod-four primes satisfies [L2] and yields a primitive representation whenever $n$ is represented.

step 1.1L2F1

3.1

Step 1.1 proves the representation criterion, step 2.1 supplies primitivity under that criterion, and step 1.2 shows that every representation has it.

step 1.1step 2.1step 1.2∎

Depends on

Used by

Squarefree sums of two squares up to 30 Example

Dependency tree · two levels

36 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, Theorems E.II.2 and E.II.4 (standard reference, not scraped)