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.
The absolute value of an integer
Definition
Let (The integers as equivalence classes of pairs of naturals). The absolute value of is
where is the order of Order on the integers and is the additive inverse supplied by The integers form a commutative ring for the operations of Arithmetic on the integers.
Why the two clauses define a function. The order on is total and antisymmetric (The integers form a totally ordered ring), so for each exactly one of and holds: totality gives at least one of and , and if both hold then by antisymmetry, in which case and fails, since means together with . The two clauses therefore never both apply and never both fail, and is a single element of because additive inverses are unique in a commutative ring: if and then .
At the boundary, by the first clause, and the second clause also gives whenever : for that is the definition, and for both readings give .
Remarks
-
This is not a second notion of absolute value. The library's other absolute value, Absolute value in an ordered field, is stated for an ordered field. The structure the construction of supplies is that of a totally ordered commutative ring (The integers form a commutative ring, The integers form a totally ordered ring), and multiplicative inverses are no part of it, so Absolute value in an ordered field does not apply here and the definition above is a new object rather than a redefinition of an existing one. (That is genuinely not a field, rather than merely not presented as one, is is a commutative monoid whose group of units is ; equivalently holds exactly for and below: its only invertible elements are and .) A general form for an ordered ring would cover both cases at once, but the definition of an ordered ring comes much later in the reading order than this page, so it is not available to reach for.
-
The two agree along the embedding of in . Write for the injective, order-preserving and arithmetic-preserving map of The integers embed in the rationals. Then is the absolute value of in the sense of Absolute value in an ordered field, the check being the same case split: preserves the order and reflects it (if but not , then by totality, so , whence and by injectivity), so exactly when , and because preserves addition. Nothing on this page rests on this observation; it is recorded so that a reader meeting twice knows the two notations are consistent, and every result below is proved for from the integer definition alone.
-
Why an absolute value is load-bearing here and not a convenience. The published division algorithm Division with remainder in : for and there are unique with and is stated for a positive divisor, so every use of it below must first replace a divisor by a positive integer, and is what that replacement produces.