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.
Powers : natural exponents in a monoid and integer exponents in a group, with
Definition
Natural exponents, in a monoid. Let be a monoid (Semigroup and monoid) and . By the recursion theorem (The recursion theorem), applied with the set , the element and the function from to , there is exactly one function , written , with
In particular for every , including , and . Since contains (The natural numbers (von Neumann)), the exponent is a genuine value of the definition and not a separate convention.
Integer exponents, in a group. Let be a group (Group and abelian group) and . Write for the embedding of The naturals embed in the integers, which is injective, preserves addition, multiplication and order, and has as image exactly the nonnegative integers. For define
- , the natural power, when and ;
- when and .
Why this is well defined. The order on is total and antisymmetric (The integers form a totally ordered ring, Order on the integers), so exactly one of and holds and the two clauses never both apply. In the first clause is nonnegative, so for some , and is unique because is injective. In the second clause gives by compatibility of the order with addition (The integers form a totally ordered ring, Arithmetic on the integers), so is a positive integer and again for a unique . The inverse is a single determined element by In a monoid, a left inverse and a right inverse of the same element are equal; hence an invertible element has exactly one inverse, and it is two-sided and Left inverse, right inverse, and invertible element of a monoid. Finally the two readings of , as a natural power and as an integer power, agree by construction, so no ambiguity is introduced.
Abbreviation. In an exponent we write for the integer when a natural number is used where an integer is expected; this is unambiguous because is injective and preserves the arithmetic and the order, and because the two readings of agree as just noted.
Additive notation. When the group is written additively the same object is written or rather than , with and ; the definitions are identical, only the symbols differ.
Remarks
-
The case split is on the integer, not on a representative. An integer is an equivalence class of pairs of naturals (The integers as equivalence classes of pairs of naturals), so a definition of by a formula in and would carry a well-definedness obligation. The definition above avoids that entirely: it splits on the sign of , which is a property of the integer itself, and then uses the unique natural supplied by The naturals embed in the integers.
-
Negative exponents need a group, not merely a monoid. The second clause uses an inverse, which a monoid need not have. Natural powers are available in any monoid, and every statement below says which of the two settings it is in.
-
The exponent is an index, an element of or of , and never an element of the group. No canonical-natural machinery (The canonical natural of a field) is involved: that item is about the image of inside a field, a different map with the same traditional name.
-
The laws , and, when and commute, are proved in Exponent laws in a group: and for all , and when and commute. The last one is false without the commuting hypothesis.
Depends on
Semigroup and monoid
Group and abelian group
Left inverse, right inverse, and invertible element of a monoid
In a monoid, a left inverse and a right inverse of the same element are equal; hence an invertible element has exactly one inverse, and it is two-sided
The recursion theorem
The natural numbers (von Neumann)
The integers as equivalence classes of pairs of naturals
Arithmetic on the integers
Order on the integers
The integers form a totally ordered ring
The naturals embed in the integers