LemmaStatement: 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.

Coprime primitively represented factors have a primitive product representation

Statement

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$ . In particular, $(a c - b d, a d + b c)$ is primitive.

Facts & Assumptions

Given: Primitive representations $P = a^{2} + b^{2}$ , $Q = c^{2} + d^{2}$ , with $\gcd (P, Q) = 1$ .

[F1]

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

[L1]

For all integers $a, b, c, d$ , $(a^{2} + b^{2}) (c^{2} + d^{2}) = (a c - b d)^{2} + (a d + b c)^{2} = (a c + b d)^{2} + (a d - b c)^{2}$ (The Brahmagupta–Fibonacci two-square identity).

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

[L2]

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

[L3]

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

Proof

technique · contradiction

1.1givenF1L1construct

Put $X = a c - b d$ and $Y = a d + b c$ . By [L1], $X^{2} + Y^{2} = P Q$ .

1.2F2L2assume-contrachoose

Suppose, for contradiction, that $(X, Y)$ is not primitive. Its positive gcd then exceeds one, so choose by [L2] a prime $ℓ$ dividing both $X$ and $Y$ .

2.1step 1.2F1L3algebra

The combinations $a X + b Y = c P$ and $a Y - b X = d P$ are divisible by $ℓ$ . Since $(c, d)$ is primitive, $ℓ$ cannot divide both; applying [L3] to the combination with coefficient not divisible by $ℓ$ gives $ℓ ∣ P$ .

2.2step 1.2F1L3algebra

Similarly, $c X + d Y = a Q$ and $c Y - d X = b Q$ . Primitivity of $(a, b)$ and [L3] give $ℓ ∣ Q$ .

3.1step 1.1step 2.1step 2.2F1F2discharge-contradiction∎

Steps 2.1 and 2.2 contradict $\gcd (P, Q) = 1$ . Hence $(X, Y)$ is primitive and, by step 1.1, primitively represents $P Q$ .

Depends on

Used by

Characterisation of primitive sums of two squares Theorem

Dependency tree · two levels

24 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, Lemma E.II.5 (standard reference, not scraped)