ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-02 (claude-opus-5)

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.

$\gcd$ at the boundary: $\gcd(a,0) = |a|$ , $\gcd(0,0) = 0$ , and the convention $\gcd(0,0) = 0$ is exactly what makes $\gcd(ca,cb) = |c|\gcd(a,b)$ true at $c = 0$

Example

The two boundary values of $\gcd$ are

$\gcd(a,0) = |a| \quad \text{for every } a, \qquad \gcd(0,0) = 0 ,$

the first by $\gcd$ is symmetric and unchanged by signs: $\gcd(a,b) = \gcd(b,a) = \gcd(|a|,|b|)$ ; moreover $\gcd(a,0) = |a|$ , $\gcd(a,1) = 1$ , $\gcd(a,a) = |a|$ , and $\gcd(a,b) \ge 1$ unless $a = b = 0$ and the second by the convention fixed in Common divisor, and the greatest common divisor $\gcd(a,b)$ , with the convention $\gcd(0,0) := 0$ . The point of this example is that the second is not free: instantiating the scaling identity $\gcd(ca,cb) = |c|\gcd(a,b)$ of $\gcd(ca, cb) = |c|\,\gcd(a,b)$ for all integers $a, b, c$ , the identity holding at $c = 0$ and at $(a,b) = (0,0)$ as well at $c = 0$ gives

$\gcd(0,0) \;=\; \gcd(0 \cdot a,\; 0 \cdot b) \;=\; |0|\,\gcd(a,b) \;=\; 0 ,$

so $0$ is the only value the identity permits. The same conclusion follows from the identity taken at $(a,b) = (0,0)$ with $c = 1+1$ : it reads $\gcd(0,0) = (1+1)\gcd(0,0)$ , and an integer $g$ with $g = g + g$ is $0$ .

Facts & Assumptions

Given: Integers $a, b, c$ .

[L1]

$\mathbb{Z}$ is a commutative ring: $x \cdot 0 = 0$ , $x + 0 = x$ , $x \cdot 1 = x$ , multiplication distributes over addition, and every $x$ has an additive inverse (The integers form a commutative ring, Arithmetic on the integers).

[L3]

$\gcd(u,0) = |u|$ for every $u$ ( $\gcd$ is symmetric and unchanged by signs: $\gcd(a,b) = \gcd(b,a) = \gcd(|a|,|b|)$ ; moreover $\gcd(a,0) = |a|$ , $\gcd(a,1) = 1$ , $\gcd(a,a) = |a|$ , and $\gcd(a,b) \ge 1$ unless $a = b = 0$ ).

[L4]

$\gcd(0,0) = 0$ by the convention of Common divisor, and the greatest common divisor $\gcd(a,b)$ , with the convention $\gcd(0,0) := 0$ , and $\gcd(u,v) \ge 0$ always.

[L5]

$\gcd(cu,cv) = |c|\gcd(u,v)$ for all $c, u, v$ ( $\gcd(ca, cb) = |c|\,\gcd(a,b)$ for all integers $a, b, c$ , the identity holding at $c = 0$ and at $(a,b) = (0,0)$ as well).

[L6]

$|0| = 0$ , and $|u| = u$ for $u \ge 0$ (The absolute value $|a|$ of an integer, Absolute value in $\mathbb{Z}$ : $|a| \ge 0$ ; $|a| = 0$ exactly when $a = 0$ ; $|-a| = |a|$ ; $|ab| = |a|\,|b|$ ; $-|a| \le a \le |a|$ ; and $|a| \le c$ exactly when $-c \le a \le c$ ).

[L7]

Every integer divides $0$ (Divisibility in $\mathbb{Z}$ : $d \mid a$ when $a = dq$ for some integer $q$ ), and every common divisor of $u$ and $v$ divides $\gcd(u,v)$ (Every common divisor of $a$ and $b$ divides $\gcd(a,b)$ ; consequently $d = \gcd(a,b)$ exactly when $d \ge 0$ , $d \mid a$ , $d \mid b$ , and every common divisor of $a$ and $b$ divides $d$ — a characterisation that holds at $(a,b) = (0,0)$ as well).

[L8]

The embedding $\iota : \mathbb{N} \to \mathbb{Z}$ has image exactly the nonnegative integers, and $\iota(1) = 1$ , $\iota(1+1) = 1+1$ since $\iota$ preserves addition (The naturals embed in the integers, The integers as equivalence classes of pairs of naturals).

Verification

technique · direct

1.1

$\gcd(a,0) = |a|$ for every $a$ , by [L3]; at $a = 0$ this reads $\gcd(0,0) = |0| = 0$ , agreeing with the convention.

L3L4L6

1.2

Instantiate [L5] at $c = 0$ : $\gcd(0 \cdot a,\, 0 \cdot b) = |0|\gcd(a,b)$ . The left side is $\gcd(0,0)$ and the right side is $0 \cdot \gcd(a,b) = 0$ , so $\gcd(0,0) = 0$ .

L1L5L6

1.3

Instantiate [L5] at $(a,b) = (0,0)$ and $c = 1+1$ : writing $g := \gcd(0,0)$ , it reads $g = |1+1|\,g$ .

2.1

An integer $g$ satisfying $g = (1+1)g = g + g$ is $0$ : adding $-g$ to both sides gives $0 = g$ . Combined with step 1.3, and with $|1+1| = 1+1$ because $1+1 = \iota(1+1)$ is nonnegative, this is a second derivation of $\gcd(0,0) = 0$ .

step 1.3L1L4L6L8

3.1

So the value $0$ is not chosen but determined, once the scaling identity is required to hold at every triple: steps 1.2 and 2.1 each force it, and step 1.1 shows it agrees with $\gcd(a,0) = |a|$ read at $a = 0$ .

step 1.1step 1.2step 2.1

4.1

The divisibility reading agrees as well: every integer divides $0$ , so every common divisor of $(0,0)$ divides $0$ , and $0$ is a common divisor of $(0,0)$ that is nonnegative — which is exactly the characterisation of $\gcd$ in [L7], returning the value $0$ .

L4L7∎

Remarks

What goes wrong without a convention is not that some identity becomes awkward but that $\gcd(0,0)$ names nothing at all: the common divisors of $(0,0)$ are all of $\mathbb{Z}$ and have no greatest element (The common divisors of $(0,0)$ are all of $\mathbb{Z}$ and have no greatest element in the order of $\mathbb{Z}$ , so $\gcd(0,0)$ cannot be defined as a maximum and is fixed by convention).
$\gcd(a,0) = |a|$ is where the absolute value earns its place. Without it the natural guess $\gcd(a,0) = a$ would be negative for negative $a$ , and $\gcd$ would fail to be nonnegative.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 62 results over 21 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Greatest common divisor (Wikipedia) (standard reference, not scraped)