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.
Divisibility in : when for some integer
Definition
Let (The integers as equivalence classes of pairs of naturals). We say divides , and write , when
the product being that of Arithmetic on the integers. We write when this fails. In this situation is called a divisor, or a factor, of , and is called a multiple of .
This is the relation the library already has, not a second one. The published Division with remainder in : for and there are unique with and introduces it in its own Statement, in these words: "We say divides , written , when for some ." Since multiplication on is commutative (The integers form a commutative ring), and are the same condition, so the definition above is that relation verbatim and the two usages agree everywhere. The theorem defined it for use on its own page and left the systematic theory to a later page; this is that page, and this item records the agreement rather than introducing a rival notion.
The remainder test. For the same Statement records that holds exactly when the remainder in , , is .
Boundary values. Each is one line from the ring axioms, and each is used below, so all three are recorded here rather than assumed:
- for every integer , including , since ;
- only for , since forces ;
- and for every , since and .
Remarks
-
The remainder test for a negative divisor is Division with remainder for any nonzero divisor: for and there are unique with and , proved next: for every , holds exactly when the remainder in , , is .
-
says a quotient exists; it says nothing on its own about the size or the sign of . Signs are irrelevant to it — , and all hold — and that is Divisibility is reflexive and transitive on , and is linear: if and then for all integers ; also implies , and . The one place where divisibility does constrain size is If and then and ; hence the set of divisors of a nonzero integer is bounded above by , and it needs the hypothesis : without it holds for arbitrarily large .
-
Notation. The bar in is a relation symbol read from left to right: the divisor is on the left. The reversed reading is a common slip, and the two directions are genuinely different, since holds while (by If and then and ; hence the set of divisors of a nonzero integer is bounded above by , with would force ).