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

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.

Stolz-Cesaro gives $(1 + 2 + \dots + n) / n^{2} \to 1 / 2$ and $(1^{p} + \dots + n^{p}) / n^{p + 1} \to 1 / (p + 1)$ for natural $p$

Example

Fix a natural number $p \geq 1$ and put

$a_{n} : = \sum_{k = 0}^{n} k^{p} = 1^{p} + 2^{p} + \dots + n^{p}, b_{n} : = n^{p + 1},$

the first equality because $0^{p} = 0$ for $p \geq 1$ (Integer powers $a^{m}$ ). Then $(b_{n})$ is strictly increasing and unbounded with $b_{0} = 0$ and $b_{n} > 0$ for $n \geq 1$ , so Stolz-Cesaro, $\infty / \infty$ form: if $b_{k}$ is strictly increasing and unbounded and $(a_{k + 1} - a_{k}) / (b_{k + 1} - b_{k}) \to L$ then $a_{k} / b_{k} \to L$ applies with $K_{0} = 1$ , and

$\lim_{n} \frac{1^{p} + 2^{p} + \dots + n^{p}}{n^{p + 1}} = \frac{1}{p + 1},$

the limit being taken over the indices $n \geq 1$ , where the quotient is defined. For $p = 1$ this is

$\lim_{n} \frac{1 + 2 + \dots + n}{n^{2}} = \frac{1}{2} .$

No closed form for $a_{n}$ is used. That is the point of the example: the difference quotient of Stolz-Cesaro replaces a summation formula by a single algebraic identity, the factorisation of $(n + 1)^{p + 1} - n^{p + 1}$ .

Facts & Assumptions

Given: A natural $p \geq 1$ , the sequences $a_{n} = \sum_{k = 0}^{n} k^{p}$ and $b_{n} = n^{p + 1}$ , and their difference quotients $d_{n} = (a_{n + 1} - a_{n}) / (b_{n + 1} - b_{n})$ .

[L1]

Stolz-Cesaro in the $\infty / \infty$ form: for $(b_{n})$ strictly increasing with range not bounded above and $(d_{n})$ convergent, the tail of $(a_{n} / b_{n})$ beyond an index where $b$ becomes positive converges to $\lim_{n} d_{n}$ (Stolz-Cesaro, $\infty / \infty$ form: if $b_{k}$ is strictly increasing and unbounded and $(a_{k + 1} - a_{k}) / (b_{k + 1} - b_{k}) \to L$ then $a_{k} / b_{k} \to L$ ); convergence depends only on a tail (Convergence depends only on the tail); limits are unique (A sequence has at most one limit).

[L2]

Powers: $a^{0} = 1$ , $a^{n + 1} = a^{n} a$ , so $0^{p} = 0$ for $p \geq 1$ (Integer powers $a^{m}$ ); $a^{m + n} = a^{m} a^{n}$ and $a^{- m} = (a^{m})^{- 1}$ for $a \neq 0$ (Laws of integer exponents); for $0 \leq a < b$ and $n \geq 1$ , $a^{n} < b^{n}$ , and $a \geq 1$ with $n \geq 1$ gives $a^{n} \geq a$ (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ).

[L3]

Factorisation: $b^{m} - a^{m} = (b - a) \sum_{k = 0}^{m - 1} a^{k} b^{m - 1 - k}$ for $m \geq 1$ (Factorisation of $b^{n} - a^{n}$ , and the resulting Lipschitz estimate).

[L4]

Finite sums and their laws (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L5]

Algebra of limits for sums, products, scalar multiples and quotients with nonvanishing denominators (Algebra of limits: sums, scalar multiples, products and quotients); convergence of real sequences (Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L6]

The Archimedean property of $R$ and its reciprocal form (Every complete ordered field is Archimedean, For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ); strict monotonicity and boundedness of real sequences (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences, Lower bound, bounded below, bounded set).

[L7]

Induction principle (The principle of mathematical induction).

[L8]

Order arithmetic: canonical naturals are positive and strictly increasing (Canonical naturals are positive and strictly increasing); a positive element has a positive inverse and reciprocation reverses the order (Inverses of positives are positive, and reciprocation reverses order); adding a constant preserves the order and inequalities add (Order is preserved by adding a constant and by adding inequalities); the order is total and transitive (Complete ordered field (least-upper-bound property), Ordered field).

Verification

technique · direct

1.1

$(b_{n})$ is strictly increasing: for naturals $m < n$ one has $0 \leq m < n$ and $p + 1 \geq 1$ , so $m^{p + 1} < n^{p + 1}$ .

L2L6L8

1.2

The range of $(b_{n})$ is not bounded above: $n \geq 1$ gives $n^{p + 1} \geq n$ , and no real bounds every canonical natural.

L2L6L8

1.3

$b_{0} = 0^{p + 1} = 0$ and $b_{n} > 0$ for $n \geq 1$ , so $K_{0} = 1$ is an index beyond which $b$ is positive.

L2L8

1.4

$a_{n + 1} - a_{n} = (n + 1)^{p}$ and $b_{n + 1} - b_{n} = (n + 1)^{p + 1} - n^{p + 1}$ , so $d_{n} = (n + 1)^{p} ((n + 1)^{p + 1} - n^{p + 1})^{- 1}$ .

L2L4

1.5

Put $τ_{n} : = n (n + 1)^{- 1}$ ; then $1 - τ_{n} = (n + 1)^{- 1}$ , so given a real $ε > 0$ and a natural $m \geq 1$ with $1 / m < ε$ one has $∣ τ_{n} - 1 ∣ = (n + 1)^{- 1} < ε$ for all $n \geq m$ , that is $\lim_{n} τ_{n} = 1$ .

L5L6L8

2.1

By the factorisation at $m = p + 1$ , $b = n + 1$ and $a = n$ : $(n + 1)^{p + 1} - n^{p + 1} = ((n + 1) - n) \sum_{k = 0}^{p} n^{k} (n + 1)^{p - k} = \sum_{k = 0}^{p} n^{k} (n + 1)^{p - k}$ .

step 1.4L3L4

2.2

By induction on $k$ , using the product rule for limits, $\lim_{n} τ_{n}^{k} = 1$ for every $k$ ; by induction on $p$ , using the sum rule, $\lim_{n} \sum_{k = 0}^{p} τ_{n}^{k} = p + 1$ .

step 1.5L5L7

3.1

Dividing numerator and denominator of $d_{n}$ by $(n + 1)^{p} > 0$ and using $n^{k} (n + 1)^{p - k} (n + 1)^{- p} = τ_{n}^{k}$ gives $d_{n} = (\sum_{k = 0}^{p} τ_{n}^{k})^{- 1}$ , and $\sum_{k = 0}^{p} τ_{n}^{k} \geq 1 > 0$ for every $n$ , the term at $k = 0$ being $1$ and all terms being $\geq 0$ .

step 1.4step 1.5step 2.1L2L4L8

4.1

Since the denominators are nonzero and their limit $p + 1$ is nonzero, the quotient rule gives $\lim_{n} d_{n} = (p + 1)^{- 1}$ .

step 2.2step 3.1L5L8

5.1

Steps 1.1, 1.2 and 4.1 are the hypotheses of Stolz-Cesaro, so the tail $j \mapsto a_{j + 1} / b_{j + 1}$ converges to $(p + 1)^{- 1}$ ; that is, $\lim_{n} (1^{p} + \dots + n^{p}) n^{- (p + 1)} = (p + 1)^{- 1}$ over the indices $n \geq 1$ .

step 1.1step 1.2step 1.3step 4.1L1

6.1

At $p = 1$ this reads $\lim_{n} (1 + 2 + \dots + n) n^{- 2} = 1 / 2$ .

step 5.1∎

Remarks

Why the limit is taken from $n = 1$ . $b_{0} = 0$ , so $a_{0} / b_{0}$ does not denote anything, and Stolz-Cesaro, $\infty / \infty$ form: if $b_{k}$ is strictly increasing and unbounded and $(a_{k + 1} - a_{k}) / (b_{k + 1} - b_{k}) \to L$ then $a_{k} / b_{k} \to L$ is stated for the tail exactly for this reason. Nothing is lost: convergence is a property of a tail (Convergence depends only on the tail).
The closed form is available and is not needed. For $p = 1$ one has $a_{n} = n (n + 1) / 2$ , and dividing by $n^{2}$ gives the limit $1 / 2$ directly. For general $p$ the closed form is Faulhaber's formula, which this library does not prove; the difference quotient sidesteps it entirely, and that is the practical content of Stolz-Cesaro.
A sanity check on the answer. The quotient compares a sum of $n$ terms, the largest of which is $n^{p}$ , with $n^{p + 1} = n \cdot n^{p}$ , so the limit must lie in $[0, 1]$ ; and the terms $k^{p}$ grow, so the sum should be a definite fraction of the largest term times $n$ . The fraction is $1 / (p + 1)$ , which is what an integral comparison would also predict. No such comparison is used above.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

59 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

Stolz-Cesàro theorem (Wikipedia) (standard reference, not scraped)
Faulhaber's formula (Wikipedia) (standard reference, not scraped)

Stolz-Cesaro gives (1+2+⋯+n)/n2→1/2(1+2+⋯+n)/n2→1/2 and (1p+⋯+np)/np+1→1/(p+1)(1p+⋯+np)/np+1→1/(p+1) for natural pp