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.
Exponentiation of natural numbers, , and its agreement with the integer power in
Definition
Let . By the recursion theorem (The recursion theorem) applied to the set , the starting element and the function (Multiplication of natural numbers), there is a unique function , written , with
Both the base and the value are natural numbers, so for all . In particular and .
Why a new item is needed. Integer powers defines for a real base , so its value is a real number. The counts on this page, and among them, are natural numbers, and an identity between them has to be an identity in . The two operations are related by clause (d) below and by nothing weaker.
(a) and for . The first is the base clause. For the second, , the clause being definitional (Multiplication of natural numbers), and every is a successor.
(b) for every . Induction: , and (Zero and one under multiplication, The principle of mathematical induction).
(c) and . Both by induction on , using associativity and commutativity of multiplication (Multiplication is associative, Multiplication is commutative). For the first, at we have , and , using (Addition of natural numbers). For the second, at both sides are , and .
(d) The bridge into . With the canonical natural (The canonical natural of a field) and the integer power of Integer powers ,
Induction on : at both sides are , since ; and , the second equality being the multiplicativity of (clause 0 of Laws of finite sums and products in , and ) and the last the recursion clause of Integer powers .
(e) is a constant product. , the -valued product of the constant list (Finite sums and finite products of natural numbers, and in ). Induction: at both sides are , and .
Definition references
Remarks
-
, and the empty product are one convention, not three. The value here is the base clause of the recursion above; by clause (e) it is the empty product of Finite sums and finite products of natural numbers, and in ; and Integer powers adopts for every real , included, so clause (d) is consistent at . The reasons for the convention are set out in Integer powers and are not repeated here.
-
The laws are the same laws. Clause (c) is the -valued form of clause 1 of Laws of integer exponents, which states , and for a base in a field. Only the two identities actually used on this page are proved above; the third is available in through clause (d) whenever it is wanted.
-
The exponent stays a natural number. Following the convention of Finite sums and finite products, by recursion, the identification of a natural with its canonical natural is deliberately not made in an exponent: in and in the exponent is a natural number, never a real.
Depends on
The recursion theorem
The principle of mathematical induction
Addition of natural numbers
Multiplication of natural numbers
Multiplication is associative
Multiplication is commutative
Zero and one under multiplication
Finite sums and finite products of natural numbers, and in
Laws of finite sums and products in , and
Integer powers
The canonical natural of a field