LemmaStatement: AI-adaptedProof: AI-adaptedSession-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.

Prime powers represented as sums of two squares

Statement

Every power of $2$ and every power of a prime $p \equiv 1 (m o d 4)$ is a sum of two squares; a power of a prime $q \equiv 3 (m o d 4)$ is representable exactly when its exponent is even. The exponent ranges over all of $N$ , including zero.

Facts & Assumptions

Given: A prime and a natural exponent.

[F1]

A representation of a nonnegative integer $n$ as a sum of two squares is an ordered pair $(x, y) \in Z^{2}$ such that $n = x^{2} + y^{2}$ (Representations and primitive representations as sums of two squares).

[L1]

The product of two nonnegative integers representable as sums of two squares is again representable as a sum of two squares (Sums of two squares are closed under products).

[L2]

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

[L3]

A prime $p$ is a sum of two integer squares if and only if $p = 2$ or $p \equiv 1 (m o d 4)$ (Fermat's two-square theorem for primes).

[L4]

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

Proof

technique · direct

1.1

For every prime $ℓ$ , the exponent-zero power is $ℓ^{0} = 1 = 1^{2} + 0^{2}$ .

F1basealgebra

1.2

If $q \equiv 3 (m o d 4)$ , every even power has the explicit representation $q^{2 j} = (q^{j})^{2} + 0^{2}$ .

F1constructalgebra

1.3

If $q^{2 j + 1} = x^{2} + y^{2}$ , then [L2] gives $x = q x_{1}$ and $y = q y_{1}$ , so $q^{2 j - 1} = x_{1}^{2} + y_{1}^{2}$ when $j \geq 1$ ; at $j = 0$ , the same divisibility would make $q^{2}$ divide $q$ , which is impossible. Induction on $j$ repeatedly reduces any alleged odd-exponent representation to that impossible base case.

F1L2L4algebradischarge-induction

2.1

The prime $2$ and every prime $p \equiv 1 (m o d 4)$ are represented by [L3]. Multiplying an induction-stage representation by the prime representation and using [L1] gives one for the next power, so [L4] represents all their natural powers.

step 1.1L1L3L4discharge-induction

3.1

Steps 1.1 and 2.1 handle $2$ and primes congruent to one modulo four, while steps 1.2 and 1.3 prove both directions for primes congruent to three modulo four.

step 1.1step 2.1step 1.2step 1.3∎

Depends on

Used by

Characterisation of positive integers that are sums of two squares Theorem

Dependency tree · two levels

16 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, §E.II.2 (standard reference, not scraped)
W. Stein, Elementary Number Theory: Primes, Congruences, and Secrets, Theorem 5.7.1 (standard reference, not scraped)