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.
Integer powers
Definition
Let , where is the ambient ordered field (Ordered field, Field).
Natural exponents. By the recursion theorem (The recursion theorem) applied to the set , the starting element and the function , there is a unique function , written , with
Thus , , and so on. Note that this is defined for every , including .
Negative exponents. If and with , set
Why that is legitimate. The right-hand side presupposes that is
invertible, that is, that . This is a proof obligation and not an
observation, and it is discharged by claim 2 of Laws of integer exponents: for
in a field, for every , proved there by induction on
from the fact that a field has no zero divisors (A field has no zero divisors: or ).
That lemma is a statement about the operation introduced here, so it depends on
this definition and is recorded in this item's justified_by rather than in its
deps (SCHEMA §3). Given , the value is a single
well-determined element, because multiplicative inverses in a field are unique
(Identities and inverses in a field are unique).
Integer exponents. Every integer (The integers as equivalence classes of pairs of naturals) is either or for a unique natural , where in these integer expressions denotes its image under the embedding (The naturals embed in the integers, Arithmetic on the integers). This too is a citation and not a slogan: the order on is total (The integers form a totally ordered ring), so or ; the image of is exactly the set of nonnegative integers, and each of them is for a unique natural (The naturals embed in the integers); and if then , by compatibility of the order with addition (The integers form a totally ordered ring), so and , with unique because is injective. The two clauses above therefore define for every whenever , and for every for arbitrary . The two exponent domains are disjoint: the natural clause handles , including , while the negative clause requires and therefore handles only .
Definition references
Remarks
- The convention is adopted here, and it is not a matter of taste but of agreement with the recursion above: is the starting value for every , exactly as the empty product is (Finite sums and finite products, by recursion). This is the convention that makes the empty product, the binomial theorem, and polynomial notation work at without an exception. The competing convention " undefined" belongs to contexts where is studied as a function of two real variables and one wants continuity, which is unavailable and irrelevant here: the exponent in is an integer, never a real.
- for every , since , a product with a zero factor (Multiplication by zero: ); and is not defined for , since has no inverse.
- The exponent is an integer and stays an integer. Rational exponents are a separate construction resting on the existence of roots (Existence and uniqueness of -th roots: a unique with , Rational powers of a positive base), and real exponents are not available at this point in the reading order; they are introduced later in Real powers for positive bases, with the zero-base positive-exponent convention ↗ (see Why real exponents are deferred on the rational-powers page).
- The laws , and are proved, not assumed, in Laws of integer exponents ↗; the order behaviour of is Monotonicity of and of .