LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

$n^{1/n} \to 1$

Statement

For a natural number $n \ge 1$ write $\iota(n) := n \cdot 1_{\mathbb{R}}$ for the canonical natural of $\mathbb{R}$ (Canonical naturals are positive and strictly increasing) and $n^{1/n} := \iota(n)^{1/n}$ , $n^{1/2} := \iota(n)^{1/2}$ for its roots (Existence and uniqueness of $n$ -th roots: a unique $a^{1/n} \ge 0$ with $(a^{1/n})^n = a$ , Rational powers $a^r$ of a positive base). Then:

$\displaystyle 1 \;\le\; n^{1/n} \;\le\; 1 + \frac{2}{n^{1/2}}$ for every natural $n \ge 1$ ;
the sequence $r_k := (k+1)^{1/(k+1)}$ , $k \in \mathbb{N}$ , converges to $1$ (Limits and Cauchy sequences of reals).

The index range is not cosmetic. The expression $n^{1/n}$ is defined only for $n \ge 1$ , since $1/n$ is not a rational number when $n = 0$ (Rational powers $a^r$ of a positive base). Sequences in this library are functions on $\mathbb{N}$ and $\mathbb{N}$ contains $0$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences), so the statement of convergence is made about the shifted family $r_k = (k+1)^{1/(k+1)}$ , which is the classical family $n^{1/n}$ , $n \ge 1$ , reindexed by $n = k+1$ . Claim 1 is stated over the natural range $n \ge 1$ where the expression means something.

Facts & Assumptions

Given: For a natural $m \ge 1$ the canonical natural $\iota(m) := m \cdot 1_{\mathbb{R}}$ , extended by $\iota(0) := 0$ ; this extension keeps the additivity $\iota(m + m') = \iota(m) + \iota(m')$ of Canonical naturals are positive and strictly increasing, which for $m$ or $m'$ equal to $0$ reads $\iota(m) = \iota(m) + 0$ .

[L1]

Roots: for real $a \ge 0$ and natural $n \ge 1$ there is a unique real $s \ge 0$ with $s^n = a$ , written $a^{1/n}$ ; it is $> 0$ when $a > 0$ , and $a^{1/1} = a$ (Existence and uniqueness of $n$ -th roots: a unique $a^{1/n} \ge 0$ with $(a^{1/n})^n = a$ , Integer powers $a^m$ ).

[L2]

Rational powers and monotonicity: $a^{1/n}$ is the rational power $a^r$ at $r = 1/n$ , and for rational $t > 0$ one has $a^t > 1$ whenever $a > 1$ ; also $\big(1/a\big)^{1/2} = 1/a^{1/2}$ for $a > 0$ (Rational powers $a^r$ of a positive base, Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ , Laws of rational exponents).

[L3]

AM-GM: for a natural $n \ge 1$ and reals $a_0, \dots, a_{n-1} \ge 0$ , the geometric mean $\big(\prod_{j<n} a_j\big)^{1/n}$ is $\le$ the arithmetic mean $\frac{1}{\iota(n)}\sum_{j<n} a_j$ (The arithmetic mean, geometric mean inequality).

[L4]

Finite sums and products: the empty sum is $0$ and the empty product $1$ ; sums and products split at any intermediate index; and $\sum_{j<m} \lambda = \iota(m)\lambda$ for a constant $\lambda$ (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L5]

Induction principle (The principle of mathematical induction).

[L6]

Canonical naturals: $\iota(m) > 0$ and $\iota(m)$ is invertible for $m \ge 1$ , $\iota$ is strictly increasing, and $\iota(2) = 2 > 1$ ; the Archimedean property gives, for every real $x$ , a natural $p \ge 1$ with $x < \iota(p)$ (Canonical naturals are positive and strictly increasing, Every complete ordered field is Archimedean).

[L7]

Order and reciprocals: $0 < a < b$ gives $0 < 1/b < 1/a$ ; multiplying an inequality by a positive element preserves it; and inequalities may be added and translated (Inverses of positives are positive, and reciprocation reverses order, Sign rules for products and monotonicity of multiplication, Order is preserved by adding a constant and by adding inequalities).

[L8]

Squares: for $a, b \ge 0$ one has $a < b$ if and only if $a \cdot a < b \cdot b$ (Monotonicity of $x \mapsto x^n$ and of $n \mapsto a^n$ , Integer powers $a^m$ ).

[L9]

Squeeze theorem, and the fact that a constant sequence converges to its value; to establish convergence it suffices to produce a threshold for every real $\varepsilon > 0$ (The squeeze theorem, Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals).

[L10]

The order on $\mathbb{N}$ is total and $\iota$ respects it (Order on the natural numbers, $\le$ is a linear order on $\mathbb{N}$ ).

Proof

technique · direct

1.1

For a natural $n \ge 1$ the element $\iota(n)$ is positive and invertible, so $\iota(n)^{1/n}$ and $\iota(n)^{1/2}$ exist and are positive.

givenL1L6

1.2

For every natural $m$ one has $\prod_{j<m} 1 = 1$ : the empty product is $1$ , and if $\prod_{j<m} 1 = 1$ then $\prod_{j<m+1} 1 = \big(\prod_{j<m} 1\big) \cdot 1 = 1$ , so this follows by induction on $m$ .

givenL4L5

2.1

For $n = 1$ one has $\iota(1) = 1$ and $1^{1/1} = 1$ ; for $n \ge 2$ one has $\iota(n) \ge \iota(2) = 2 > 1$ and $1/n$ is a positive rational, so $\iota(n)^{1/n} > 1$ . In either case $n^{1/n} \ge 1$ .

step 1.1L1L2L6L10

2.2

Let $n \ge 2$ and put $u := \iota(n)^{1/2}$ , so that $u > 0$ and $u \cdot u = \iota(n)$ . Apply [L3] to the list of $n$ nonnegative reals given by $a_0 = a_1 = u$ and $a_j = 1$ for $2 \le j < n$ , the latter range being empty when $n = 2$ . Splitting at index $2$ gives $\prod_{j<n} a_j = \big(\prod_{j<2} a_j\big)\big(\prod_{j<n-2} a_{2+j}\big) = (u \cdot u) \cdot 1 = \iota(n)$ by step 1.2, so the geometric mean is $\iota(n)^{1/n}$ ; and $\sum_{j<n} a_j = \big(\sum_{j<2} a_j\big) + \big(\sum_{j<n-2} 1\big) = (u + u) + \iota(n-2) = (u+u) + \iota(n) - 2$ , using additivity of $\iota$ and $\iota(2) = 2$ , so the arithmetic mean is $A = \big((u+u) + \iota(n) - 2\big)/\iota(n) = 1 + \big((u+u) - 2\big)/\iota(n)$ . Since $(u+u) - 2 < u + u$ and $\iota(n) > 0$ , and $(u+u)/\iota(n) = (u+u)/(u \cdot u) = 2/u$ , this gives $\iota(n)^{1/n} \le A \le 1 + 2/u = 1 + 2/n^{1/2}$ .

step 1.1step 1.2L1L3L4L6L7algebra

2.3

For $n = 1$ the same bound holds trivially: $1^{1/1} = 1 \le 1 + 2 = 1 + 2/1^{1/2}$ .

step 1.1L1L6L7

2.4

The sequence $b_k := 1 + 2/(k+1)^{1/2}$ converges to $1$ . Given a real $\varepsilon > 0$ , put $t := 2/\varepsilon > 0$ and take a natural $p \ge 1$ with $t \cdot t < \iota(p)$ . For $k \ge p$ we have $k + 1 > p$ , hence $\iota(k+1) > \iota(p) > t \cdot t$ , and since $\big(\iota(k+1)^{1/2}\big)\big(\iota(k+1)^{1/2}\big) = \iota(k+1)$ with both factors $\ge 0$ , this forces $t < \iota(k+1)^{1/2}$ . Therefore $0 < 2/\iota(k+1)^{1/2} < 2/t = \varepsilon$ , that is $|b_k - 1| < \varepsilon$ .

step 1.1L1L6L7L8L9L10algebra

3.1

Claim 1 is the combination of steps 2.1, 2.2 and 2.3, the two upper bounds covering $n \ge 2$ and $n = 1$ respectively.

step 2.1step 2.2step 2.3

4.1

For every $k \in \mathbb{N}$ the natural $k+1$ is $\ge 1$ , so claim 1 gives $1 \le r_k \le b_k$ . The constant sequence $1$ converges to $1$ and $(b_k)$ converges to $1$ by step 2.4, so the squeeze theorem gives $r_k \to 1$ , which is claim 2.

step 3.1step 2.4L9∎

Remarks

Where the $\sqrt{n}$ comes from. AM-GM is applied to a list whose product is $n$ but whose entries are as close to $1$ as possible: two copies of $n^{1/2}$ and $n-2$ copies of $1$ . The arithmetic mean is then $1 + (2n^{1/2} - 2)/n$ , which tends to $1$ at the rate $2/n^{1/2}$ . Splitting $n$ as $n^{1/2} \cdot n^{1/2}$ rather than as $n \cdot 1$ is the whole trick: the list $n, 1, \dots, 1$ gives only $n^{1/n} \le 2 - 1/n$ , which does not converge to $1$ .
The lower bound is not decoration. Without $n^{1/n} \ge 1$ the squeeze has nothing below it, and the upper bound alone would leave open a limit smaller than $1$ . It comes from monotonicity of rational powers in the base (Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ ) and holds with equality only at $n = 1$ .
No logarithm and no exponential is used. The usual quick proof writes $n^{1/n} = e^{(\log n)/n}$ and appeals to $(\log n)/n \to 0$ ; neither function exists in this library yet, and the AM-GM route needs nothing beyond roots and finite sums.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 94 results over 29 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Nth root (Wikipedia) (standard reference, not scraped)
AM-GM inequality (Wikipedia) (standard reference, not scraped)
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)

n1/n→1n^{1/n} \to 1n1/n→1