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

If $4$ divides $x^{2} + y^{2} + z^{2}$ then $x$ , $y$ and $z$ are all even

Statement

Let $x, y, z \in Z$ and suppose $4 ∣ x^{2} + y^{2} + z^{2}$ (Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ). Then $x$ , $y$ and $z$ are all even.

Facts & Assumptions

Given: Integers $x, y, z$ with $4 ∣ x^{2} + y^{2} + z^{2}$ .

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

[F2]

For $d, a \in Z$ , $d ∣ a$ means $a = d q$ for some $q \in Z$ (Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ).

[L1]

For every integer $x$ : if $x$ is odd then $x^{2} \equiv 1 (m o d 4)$ , and if $x$ is even then $x^{2} \equiv 0 (m o d 4)$ (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)$ and $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 · direct

1.1givenL3construct

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 one of $0, 1, 2, 3$ .

1.2L1

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

2.1step 1.1step 1.2L2F1algebra

Adding the three contributions by [L2], $x^{2} + y^{2} + z^{2} \equiv t (m o d 4)$ , since the $t$ odd coordinates each contribute $1$ and the remaining ones contribute $0$ .

3.1givenstep 2.1L2F1F2algebra

The hypothesis $4 ∣ x^{2} + y^{2} + z^{2}$ says $x^{2} + y^{2} + z^{2} \equiv 0 (m o d 4)$ by [F1] and [F2]; subtracting this from step 2.1 by the difference clause of [L2] gives $0 \equiv t (m o d 4)$ , that is $4 ∣ t$ .

4.1step 1.1step 3.1L3algebra∎

Since $0 \leq t < 4$ , [L3] applied with $a = t$ and $b = 4$ has the unique pair $(q, r) = (0, t)$ , and it says $4 ∣ t$ holds exactly when $r = 0$ ; so step 3.1 forces $t = 0$ , meaning none of $x, y, z$ is odd, that is $x$ , $y$ and $z$ are all even.

Remarks

The modulus cannot be relaxed to $2$ . Divisibility of $x^{2} + y^{2} + z^{2}$ by $2$ leaves $t = 0$ and $t = 2$ both possible, and $1^{2} + 1^{2} + 0^{2} = 2$ realises the second, so $2$ dividing the sum does not force the coordinates even. It is the count $t$ being pinned to a single residue modulo $4$ that makes the argument work, and that needs the modulus $4$ .

Where it is used. This is the halving step of Positive integers $4^{a} m$ with $m \equiv 7 (m o d 8)$ are not sums of three integer squares: it is what licenses passing from a representation of $4^{σ (a)} m$ to one of $4^{a} m$ .

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 (standard reference, not scraped)

If 44 divides x2+y2+z2x2+y2+z2 then xx, yy and zz are all even