ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26

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.

The four standard limits $n^{1 / n} \to 1$ , $a^{1 / n} \to 1$ , $n^{α} / (1 + p)^{n} \to 0$ and $x^{k} / k! \to 0$ , computed

Example

The four standard limits of this page, written as sequences on $N$ and instantiated. Throughout $ι (n) = n \cdot 1_{R}$ is the canonical natural, with $ι (0) = 0$ .

classical form	as a sequence on $N$	value	source
$n^{1 / n} \to 1$	$(k + 1)^{1 / (k + 1)}$	$1$	$n^{1 / n} \to 1$
$a^{1 / n} \to 1$ , $a > 0$	$a^{1 / (k + 1)}$	$1$	For every $a > 0$ , $a^{1 / n} \to 1$
$n^{α} / (1 + p)^{n} \to 0$	$ι (k)^{α} / (1 + p)^{k}$	$0$	For every $p > 0$ and every positive rational $α$ , $n^{α} / (1 + p)^{n} \to 0$
$x^{k} / k! \to 0$	$x^{k} / k!$	$0$	For every real $x$ , $x^{k} / k! \to 0$

Two of the four need an index shift and two do not, and the reason is visible in the classical forms: in the first two the index sits in the exponent as $1 / n$ , which is not a rational number at $n = 0$ , so those families begin at $n = 1$ and are written here with $n = k + 1$ . In the last two the index sits in the base or in a factorial, both of which are defined at $0$ , so no shift is needed and the sequences begin at $k = 0$ with the values $0$ and $1$ respectively.

The instances computed below are:

$2^{1 / (k + 1)} \to 1, \frac{ι (k)^{2}}{2^{k}} \to 0, \frac{2^{k}}{k!} \to 0, \frac{(- 3)^{k}}{k!} \to 0, \frac{ι (k)^{2}}{k!} \to 0.$

The last of these is not one of the four; it is the composite that orders the three scales, and it is obtained from two of them by the product rule.

Facts & Assumptions

Given: The canonical naturals $ι (n) = n \cdot 1_{R}$ with $ι (0) = 0$ ; the factorial $k! = \prod_{j < k} ι (j + 1)$ of For every real $x$ , $x^{k} / k! \to 0$ ; rational powers (Rational powers $a^{r}$ of a positive base) and integer powers (Integer powers $a^{m}$ ).

[L1]

$(k + 1)^{1 / (k + 1)} \to 1$ , with $1 \leq n^{1 / n} \leq 1 + 2 / n^{1 / 2}$ for every natural $n \geq 1$ ( $n^{1 / n} \to 1$ ).

[L2]

For every real $a > 0$ , $a^{1 / (k + 1)} \to 1$ ; and for real $b \geq 1$ and natural $n \geq 1$ , $1 \leq b^{1 / n} \leq 1 + (b - 1) / ι (n)$ (For every $a > 0$ , $a^{1 / n} \to 1$ ).

[L3]

For every real $p > 0$ and rational $α > 0$ , $ι (k)^{α} / (1 + p)^{k} \to 0$ (For every $p > 0$ and every positive rational $α$ , $n^{α} / (1 + p)^{n} \to 0$ ).

[L4]

For every real $x$ , $x^{k} / k! \to 0$ (For every real $x$ , $x^{k} / k! \to 0$ ).

[L5]

Algebra of limits: products of convergent sequences converge to the product of the limits (Algebra of limits: sums, scalar multiples, products and quotients, Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L6]

Arithmetic: $0 < 1 < 2 < 3$ , so $1$ , $2$ , $3 / 2$ and $1 / 2$ are positive and $2 = 1 + 1$ , $3 / 2 = 1 + 1 / 2$ ; a positive integer power of a positive real is positive and nonzero; $2$ is a positive rational and $1 / 2$ is a positive rational (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication, Canonical naturals are positive and strictly increasing, Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ , Finite sums and finite products, by recursion, Ordered field, Complete ordered field (least-upper-bound property)).

Verification

technique · direct

1.1

The first standard limit gives $(k + 1)^{1 / (k + 1)} \to 1$ , together with the explicit two-sided bound $1 \leq (k + 1)^{1 / (k + 1)} \leq 1 + 2 / (k + 1)^{1 / 2}$ valid at every $k \in N$ , since $k + 1 \geq 1$ .

givenL1

1.2

The second gives $2^{1 / (k + 1)} \to 1$ and $(1 / 2)^{1 / (k + 1)} \to 1$ , both bases being positive; for the first of these the explicit bound of [L2] with $b = 2$ reads $1 \leq 2^{1 / n} \leq 1 + 1 / ι (n)$ for every natural $n \geq 1$ .

givenL2L6

1.3

The third, with $p = 1$ and $α = 2$ , gives $ι (k)^{2} / 2^{k} \to 0$ ; with $p = 1 / 2$ and $α = 1 / 2$ it gives $ι (k)^{1 / 2} / (3 / 2)^{k} \to 0$ . Both $p$ are positive reals and both $α$ are positive rationals, so [L3] applies in each case.

givenL3L6

1.4

The fourth, with $x = 2$ and with $x = - 3$ , gives $2^{k} / k! \to 0$ and $(- 3)^{k} / k! \to 0$ ; no hypothesis on $x$ is needed, in particular no positivity.

givenL4

2.1

Multiplying the first limit of step 1.3 by the first of step 1.4 and using $2^{k} \neq 0$ gives $ι (k)^{2} / k! = (ι (k)^{2} / 2^{k}) (2^{k} / k!) \to 0 \cdot 0 = 0$ .

step 1.3step 1.4L5L6

2.2

Multiplying the limit of step 1.1 by the first of step 1.2 gives $(k + 1)^{1 / (k + 1)} 2^{1 / (k + 1)} \to 1 \cdot 1 = 1$ .

step 1.1step 1.2L5

3.1

The four limits and the two composites are therefore established as displayed, and together they order the three growth scales: a fixed power of $n$ is beaten by every geometric sequence of ratio $> 1$ by step 1.3, every geometric sequence is beaten by the factorial by step 1.4, and consequently a fixed power of $n$ is beaten by the factorial by step 2.1.

step 1.1step 1.2step 1.3step 1.4step 2.1step 2.2∎

Remarks

The two bounds quoted in steps 1.1 and 1.2 are the useful part in practice. They convert the qualitative statement into a rate: $n^{1 / n}$ is within $2 / n^{1 / 2}$ of $1$ , and $a^{1 / n}$ within $(a - 1) / n$ of $1$ when $a \geq 1$ . The second rate is faster, and the difference is real: in $n^{1 / n}$ the base itself grows with the index.
Why $α$ is rational and $p$ is real. The exponent $α$ must be rational because rational powers are all this library has; the base $1 + p$ may be any real $> 1$ because it is raised only to integer powers. The asymmetry is a fact about what has been constructed, not about the mathematics, and it disappears once real exponents are available.
The composite in step 2.1 is the one usually quoted as "factorials beat polynomials". It is not proved directly anywhere on this page: it is the product of two of the four standard limits, and the product rule (Algebra of limits: sums, scalar multiples, products and quotients) is what assembles it.
Nothing here uses $lim sup$ . All four are ordinary limits, and the page's machinery is needed only to prove them, not to state them; the connection to the rest of the page is that For $a_{k} > 0$ : $lim inf a_{k + 1} / a_{k} \leq lim inf a_{k}^{1 / k} \leq lim sup a_{k}^{1 / k} \leq lim sup a_{k + 1} / a_{k}$ is the tool that makes several of them routine once one of them is known.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

65 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

W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (3.20) (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §6.5 (standard reference, not scraped)
Limit of a sequence (Wikipedia) (standard reference, not scraped)

The four standard limits n1/n→1n1/n→1, a1/n→1a1/n→1, nα/(1+p)n→0nα/(1+p)n→0 and xk/k!→0xk/k!→0, computed