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.
Common divisor, and the greatest common divisor , with the convention
Definition
Let . An integer is a common divisor of and when and (Divisibility in : when for some integer ). Write
for the set of common divisors.
Case : the greatest element exists. is nonempty, since and for every and (Divisibility in : when for some integer ). It is bounded above: at least one of and is nonzero, say (if instead , argue with throughout), and every divides , so by If and then and ; hence the set of divisors of a nonzero integer is bounded above by . A nonempty set of integers bounded above has a unique greatest element (A nonempty set of integers bounded above has a greatest element, and a nonempty set of integers bounded below has a least element), and we define
Since and is greatest, ; in particular .
Case : a convention, fixed here. Every integer divides (Divisibility in : when for some integer ), so , which has no greatest element at all: the clause above defines nothing, and leaving undefined would put a hole in every identity below. We therefore set
With both cases together, is defined for every pair of integers, and always.
Why , and not some other value. The convention is not arbitrary, and the reasons are recorded here rather than deferred:
- It is the greatest common divisor in the divisibility ordering. is a common divisor of and , and every common divisor of and divides . So is greatest at in the sense "divisible by every common divisor", which is the sense that Every common divisor of and divides ; consequently exactly when , , , and every common divisor of and divides — a characterisation that holds at as well shows holds at every pair, included, whereas "greatest in the order of " fails there.
- It is the only value under which the scaling identity extends to this boundary. Requiring to hold at every triple leaves no freedom here. At with any it would read , whose right-hand side does not involve at all; and at with it reads , again giving . The value is therefore chosen here, and for all integers , the identity holding at and at as well then proves the identity for every triple with this convention in force; its own case reads the value off this definition rather than establishing it.
- It is consistent with the product formula — (Every common multiple of and is a multiple of , and ) reads at , using from Common multiple, and the least common multiple , taken to be when or . This one is a check, not a second forcing argument: with the left side vanishes whatever value is given, so the product formula is silent at and only the scaling identity above pins the value down.
Remarks
-
The gap the convention fills is real. The failure is exhibited on the companion page by The common divisors of are all of and have no greatest element in the order of , so cannot be defined as a maximum and is fixed by convention ↗: the common divisors of really are all of , and really have no greatest element, so a value has to be supplied rather than computed.
-
The definition is by a maximum, and the theory replaces it by a divisibility characterisation. Reading as "largest common divisor" is what makes the case awkward, and it is also not the property later pages use. Every common divisor of and divides ; consequently exactly when , , , and every common divisor of and divides — a characterisation that holds at as well proves the replacement: exactly when , is a common divisor, and every common divisor divides . That statement is uniform across all pairs.
-
Sign. is never negative, by construction. Since is a common divisor whenever is (Divisibility is reflexive and transitive on , and is linear: if and then for all integers ; also implies , and ), the set is symmetric about , and taking the greatest element is exactly the choice of the nonnegative representative from each pair of associates (For integers and the following are equivalent: and ; for a unit ; . Being associates is an equivalence relation whose class of is ).
-
Two arguments, not a list. is defined here on pairs only. Nothing on this page needs a greatest common divisor of a longer list, and none is defined.
Depends on
Divisibility in : when for some integer
If and then and ; hence the set of divisors of a nonzero integer is bounded above by
A nonempty set of integers bounded above has a greatest element, and a nonempty set of integers bounded below has a least element
The absolute value of an integer
Order on the integers
The integers form a totally ordered ring