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.

Two essentially different two-square representations factor an odd integer

Statement

Let $N$ be odd and suppose

$N = x^{2} + y^{2} = u^{2} + v^{2},$

where $x, u$ are positive odd integers, $y, v$ are positive even integers, and $0 < x < u$ . Then $0 < v < y$ , and two essentially different normalized representations force a factorisation $N = P Q$ with $P, Q > 1$ . More precisely, there are positive integers $e, f, g, h$ such that

$x = e g - f h, y = f g + e h, u = e g + f h, v = f g - e h,$

and $N = (e^{2} + f^{2}) (g^{2} + h^{2})$ .

Facts & Assumptions

Given: The two normalized representations and inequalities in the Statement.

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

[F1]

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]

If $\gcd (a, b) = 1$ and $a ∣ b c$ , then $a ∣ c$ (If $\gcd (a, b) = 1$ and $a ∣ b c$ then $a ∣ c$ ; and if $a ∣ c$ , $b ∣ c$ and $\gcd (a, b) = 1$ then $a b ∣ c$ ).

Proof

technique · direct

1.1

Since $u^{2} - x^{2} = y^{2} - v^{2} > 0$ , one has $0 < v < y$ , and $(u - x) (u + x) = (y - v) (y + v)$ . All four factors are positive and even, so with $A = (u + x) / 2$ , $B = (u - x) / 2$ , $C = (y + v) / 2$ , and $D = (y - v) / 2$ one has $A B = C D$ .

givenalgebra

2.1

Let $g = \gcd (A, C)$ and write $A = e g$ , $C = f g$ . Positivity gives $e, f, g > 0$ , and $\gcd (e, f) = 1$ , since a common divisor greater than one would make a common divisor of $A, C$ larger than $g$ .

step 1.1F1choose

3.1

The equality $A B = C D$ becomes $e B = f D$ . Since $\gcd (e, f) = 1$ , [L2] gives $e ∣ D$ and $f ∣ B$ ; write $D = e h$ and $B = f h$ with $h > 0$ .

step 1.1step 2.1L2algebra

4.1

From $A = e g$ , $B = f h$ , $C = f g$ , and $D = e h$ one obtains $u = A + B = e g + f h$ , $x = A - B = e g - f h$ , $y = C + D = f g + e h$ , and $v = C - D = f g - e h$ .

step 2.1step 3.1algebra

5.1

By [L1], $(e^{2} + f^{2}) (g^{2} + h^{2}) = (e g + f h)^{2} + (f g - e h)^{2} = u^{2} + v^{2} = N$ . Each factor exceeds one because all four entries are positive.

step 4.1L1algebra∎

Depends on

Used by

Dependency tree · two levels

15 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, Theorem E.I.3 (standard reference, not scraped)