Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicable
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 am

Definition

Let a∈R, where R is the ambient ordered field (Ordered field, Field).

Natural exponents. By the recursion theorem (The recursion theorem) applied to the set R, the starting element 1 and the function f(x)=x⋅a, there is a unique function N→R, written n↦an, with

a0=1,an+1=an⋅a(n∈N).

Thus a1=a, a2=a⋅a, and so on. Note that this is defined for every a, including a=0.

Negative exponents. If a≠0 and n∈N with n≥1, set

a−n:=(an)−1.

Why that is legitimate. The right-hand side presupposes that an is invertible, that is, that an≠0. This is a proof obligation and not an observation, and it is discharged by claim 2 of Laws of integer exponents: for a≠0 in a field, an≠0 for every n∈N, proved there by induction on n from the fact that a field has no zero divisors (A field has no zero divisors: ab=0⇒a=0 or b=0). 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 an≠0, the value (an)−1 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 m (The integers as equivalence classes of pairs of naturals) is either n or −n for a unique natural n, where n in these integer expressions denotes its image under the embedding ι:N→Z (The naturals embed in the integers, Arithmetic on the integers). This too is a citation and not a slogan: the order on Z is total (The integers form a totally ordered ring), so m≥0 or m<0; the image of ι is exactly the set of nonnegative integers, and each of them is n for a unique natural n (The naturals embed in the integers); and if m<0 then −m>0, by compatibility of the order with addition (The integers form a totally ordered ring), so −m=n and m=−n, with n unique because ι is injective. The two clauses above therefore define am for every m∈Z whenever a≠0, and for every m∈N for arbitrary a. The two exponent domains are disjoint: the natural clause handles m≥0, including m=0, while the negative clause requires n≥1 and therefore handles only m<0.

Remarks

Depends on

Dependency tree · 2 levels

Sources