LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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.

No sum of three integer squares is congruent to $7$ modulo $8$

Statement

There are no integers $x, y, z$ with $x^{2} + y^{2} + z^{2} \equiv 7 (m o d 8)$ (Congruence modulo an integer: $a \equiv b (m o d n)$ when $n ∣ (a - b)$ , including the moduli $0$ and $1$ ). In fact, the residues modulo $8$ attained by sums of three integer squares are exactly $0, 1, 2, 3, 4, 5, 6$ .

Facts & Assumptions

Given: Integers $x, y, z$ .

[F1]

For $a, b, n \in Z$ , $a \equiv b (m o d n)$ means $n ∣ (a - b)$ (Congruence modulo an integer: $a \equiv b (m o d n)$ when $n ∣ (a - b)$ , including the moduli $0$ and $1$ ).

[L1]

For every integer $x$ : if $x$ is odd then $x^{2} \equiv 1 (m o d 8)$ , and if $x$ is even then $x^{2} \equiv 0 (m o d 8)$ or $x^{2} \equiv 4 (m o d 8)$ (A square is congruent to $0$ , $1$ or $4$ modulo $8$ ).

[L2]

If $a \equiv a^{'} (m o d n)$ and $b \equiv b^{'} (m o d n)$ , then $a + b \equiv a^{'} + b^{'} (m o d n)$ (Congruent integers may be added, subtracted and multiplied: representative changes preserve both arithmetic operations).

[L3]

For $a, b \in Z$ with $b \neq 0$ there is exactly one pair $(q, r)$ of integers with $a = q b + r$ and $0 \leq r < ∣ b ∣$ ; moreover $b ∣ a$ holds exactly when $r = 0$ (Division with remainder for any nonzero divisor: for $a \in Z$ and $b \neq 0$ there are unique $q, r \in Z$ with $a = q b + r$ and $0 \leq r < ∣ b ∣$ ).

Proof

technique · cases

1.1

By [L3] with $b = 2$ each of $x, y, z$ is even or odd; let $t$ be how many of the three are odd, so $t$ is $0$ , $1$ , $2$ or $3$ , and these four values exhaust the possibilities.

givenL3construct

1.2

By [L1], each odd coordinate contributes a square congruent to $1$ modulo $8$ , and each even coordinate contributes a square congruent to $0$ or to $4$ modulo $8$ .

2.1

If $t = 3$ then, adding the three contributions by [L2], $x^{2} + y^{2} + z^{2} \equiv 1 + 1 + 1 = 3 (m o d 8)$ .

step 1.1step 1.2assume-case threeL2F1algebra

2.2

If $t = 2$ then $x^{2} + y^{2} + z^{2} \equiv 1 + 1 + e (m o d 8)$ with $e$ equal to $0$ or $4$ , so the sum is congruent to $2$ or to $6$ .

step 1.1step 1.2assume-case twoL2F1algebra

2.3

If $t = 1$ then $x^{2} + y^{2} + z^{2} \equiv 1 + e_{1} + e_{2} (m o d 8)$ with each $e_{i}$ equal to $0$ or $4$ , giving $1$ , $5$ , $5$ or $9$ ; since $9 \equiv 1 (m o d 8)$ , the sum is congruent to $1$ or to $5$ .

step 1.1step 1.2assume-case oneL2F1algebra

2.4

If $t = 0$ then $x^{2} + y^{2} + z^{2} \equiv e_{1} + e_{2} + e_{3} (m o d 8)$ with each $e_{i}$ equal to $0$ or $4$ , giving $0$ , $4$ , $8$ or $12$ ; since $8 \equiv 0$ and $12 \equiv 4$ modulo $8$ , the sum is congruent to $0$ or to $4$ .

step 1.1step 1.2assume-case zeroL2F1algebra

3.1

Steps 2.1 to 2.4 cover the four values of $t$ listed in step 1.1 and show that every sum of three squares is congruent to one of $0, 1, 2, 3, 4, 5, 6$ , never to $7$ , modulo $8$ . Conversely, the triples $(0, 0, 0)$ , $(1, 0, 0)$ , $(1, 1, 0)$ , $(1, 1, 1)$ , $(2, 0, 0)$ , $(2, 1, 0)$ and $(2, 1, 1)$ have sums of squares $0, 1, 2, 3, 4, 5, 6$ , respectively. Thus the attained residues are exactly the seven listed classes, and $7$ is not attained.

step 2.1step 2.2step 2.3step 2.4F1algebracases-exhaustive∎

Remarks

Why the cases are counted by parity rather than listed by value. Enumerating the possible triples of residues from ${0, 1, 4}$ would give ten unordered choices; grouping them by how many coordinates are odd gives four, because the odd coordinates contribute a fixed residue and only the even ones branch. The exhaustiveness is then visible from step 1.1 alone.

Every listed residue is attained. Taking $(x, y, z)$ to be $(0, 0, 0)$ , $(1, 0, 0)$ , $(1, 1, 0)$ , $(1, 1, 1)$ , $(2, 0, 0)$ , $(2, 1, 0)$ and $(2, 1, 1)$ gives sums $0, 1, 2, 3, 4, 5, 6$ , so the second sentence of the Statement is an equality of sets and not merely an inclusion.

Depends on

Used by

7 and 28 are not sums of three integer squares Counterexample
Positive integers 4ᵃ m with m≡ 7 (mod 8) are not sums of three integer squares Proposition

Dependency tree · two levels

17 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

Evan Dummit, Number Theory (part 9): The Geometry of Numbers, §9.1.3 (standard reference, not scraped)
Karl-Dieter Crisman, Number Theory: In Context and Interactive, §14.2, Fact 14.2.1 (standard reference, not scraped)

No sum of three integer squares is congruent to 77 modulo 88