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 .
Depends on
- The recursion theorem
- Ordered field
- The integers as equivalence classes of pairs of naturals
- Field
- Arithmetic on the integers
- The naturals embed in the integers
- Identities and inverses in a field are unique
- A field has no zero divisors: $ab = 0 \Rightarrow a = 0$ or $b = 0$
- Multiplication by zero: $0 \cdot a = 0$
- The integers form a totally ordered ring
Used by
- Bias-corrected Adam update Algorithm
- Bias-corrected AMSGrad update Algorithm
- Unanchored Levenberg–Marquardt step with explicit early stopping Algorithm
- ∑_k<n+1C(n, k) = 2ⁿ, and ∑_k<n+1(-1)ᵏiotaC(n, k) = 0 for n ≥ 1 Corollary
- If f,g are integrable on [a,b] then so are | f|, f², fg, max(f,g) and min(f,g), and |∫ₐᵇ f| ≤ ∫ₐᵇ| f| Corollary
- L(1/x)=-L(x), L(xⁿ)=nL(x), and in particular L(2ⁿ)=nL(2) Corollary
- Raabe is Kummer with ζₖ = k+1: for positive terms, liminf (k+1)(aₖ/aₖ₊₁ - 1) > 1 gives convergence and limsup < 1 gives divergence Corollary
- The a priori bound d(x^*, xₙ) ≤ qⁿ d(x₁,x₀)/(1-q) and the a posteriori bound d(x^*, xₙ₊₁) ≤ q d(xₙ₊₁,xₙ)/(1-q) Corollary
- The Lagrange and Cauchy forms of Taylor's remainder Corollary
- The symmetric Lovász Local Lemma under ep(d+1)≤1 Corollary
- Volume doubling under a nonnegative ricci lower bound Corollary
- Whenever the ratio test decides, the root test decides the same way, and the converse fails Corollary
- ι(Dₙ) = ι(n) ι(Dₙ₋₁) + (-1)ⁿ for n ≥ 1, and Dₙ = (n-1)(Dₙ₋₁ + Dₙ₋₂) for n ≥ 2 Corollary
- ‖·‖₁ on ℝ² violates the parallelogram law, so no symmetric bilinear form induces it Counterexample
- ∏_j ≥ 0 (1 + (-1)ʲ/√j+2) has partial products tending to 0 although ∑_j ≥ 0 (-1)ʲ/√j+2 converges Counterexample
- 1/4 lies in the Cantor set and is the endpoint of no removed interval, so the endpoints do not exhaust it Counterexample
- A bounded continuous normalized function that is not of positive type Counterexample
- A curve for which the mean value inequality is an equality, showing the constant cannot be improved Counterexample
- A function differentiable on [0,1] whose derivative is unbounded, hence not Riemann integrable Counterexample
- A nonnegative non-monotone sequence for which ∑ aₖ and ∑ 2ᵏ a_2ᵏ behave differently Counterexample
- A three-set count that drops the triple intersection and returns the wrong answer Counterexample
- Adam diverges on a periodic bounded-gradient loss sequence Counterexample
- aₖ = 2^-k+(-1)ᵏ has ratio limsup 2 and liminf 1/8, so the ratio test fails, while the root test gives convergence Counterexample
- Bernoulli fails for x < -1: x = -4, n = 3 Counterexample
- Continuous f and integrable sign-changing g with ∫ₐᵇ fg ≠ f(ξ)∫ₐᵇ g for every ξ Counterexample
- Continuous fₙ → 0 pointwise on [0,1] with ∫₀¹ fₙ = 1 for every n Counterexample
- Dini's theorem fails for a discontinuous limit: powers on [0,1] decrease pointwise to a discontinuous endpoint indicator but not uniformly Counterexample
- f(t) = (t², t³) on [0,1]: no ξ satisfies f(1)-f(0) = f'(ξ) Counterexample
- Finite thresholds rule out an r-independent VC covering bound Counterexample
- Finite variance does not imply a sub-Gaussian tail Counterexample
- fₖ(x)=xᵏ⁺¹ converges pointwise but not uniformly on [0,1] Counterexample
- g(x,y) = xy/(x²+y²), extended by g(0,0)=0, is continuous in each variable separately and not continuous at the origin Counterexample
- Minkowski fails for p = 1/2: the hypothesis p ≥ 1 is load-bearing Counterexample
- Null times divergent has no rule: xₖ = 1/k with yₖ = ck gives product limit c, and with yₖ = k² gives divergence Counterexample
- On a closed interval of ℚ there is a continuous unbounded function, a bounded one with no maximum, and one without the intermediate value property Counterexample
- Over ℚ there is a nonconstant differentiable function with identically zero derivative, so Rolle and the mean value theorem both fail Counterexample
- Point evaluation is unbounded below the Sobolev continuity threshold Counterexample
- ℝ is the union of a meager set and a set of measure zero, so smallness of category and smallness of measure are independent notions Counterexample
- Taking out an unbounded factor needs integrability Counterexample
- The convergence (1+x/n)ⁿ→exp x is not uniform on ℝ Counterexample
…and 256 more results.
Dependency tree · two levels
27 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- J. Aspnes, Summation Notation (standard reference, not scraped)
- M. Fochler, Recursive sums, products, and powers (standard reference, not scraped)
- Exponentiation (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
- T. Tao, Analysis I, 3rd ed., §4.3 (standard reference, not scraped)