ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck 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 (c a, c b) = ∣ c ∣ \gcd (a, b)$ true at $c = 0$

Example

The two boundary values of $\gcd$ are

$\gcd (a, 0) = ∣ a ∣ for every a, \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) \geq 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 (c a, c b) = ∣ c ∣ \gcd (a, b)$ of $\gcd (c a, c b) = ∣ 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]

$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) \geq 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) \geq 0$ always.

[L5]

$\gcd (c u, c v) = ∣ c ∣ \gcd (u, v)$ for all $c, u, v$ ( $\gcd (c a, c b) = ∣ 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 \geq 0$ (The absolute value $∣ a ∣$ of an integer, Absolute value in $Z$ : $∣ a ∣ \geq 0$ ; $∣ a ∣ = 0$ exactly when $a = 0$ ; $∣ - a ∣ = ∣ a ∣$ ; $∣ a b ∣ = ∣ a ∣ ∣ b ∣$ ; $- ∣ a ∣ \leq a \leq ∣ a ∣$ ; and $∣ a ∣ \leq c$ exactly when $- c \leq a \leq c$ ).

[L7]

Every integer divides $0$ (Divisibility in $Z$ : $d ∣ a$ when $a = d q$ 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 \geq 0$ , $d ∣ a$ , $d ∣ 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 $ι : N \to Z$ has image exactly the nonnegative integers, and $ι (1) = 1$ , $ι (1 + 1) = 1 + 1$ since $ι$ 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 = ι (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 $Z$ and have no greatest element (The common divisors of $(0, 0)$ are all of $Z$ and have no greatest element in the order of $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 · two levels

35 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

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

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