ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck 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 \ge 1$ and put

$a_n \;:=\; \sum_{k=0}^{n} k^p \;=\; 1^p + 2^p + \dots + n^p, \qquad b_n \;:=\; n^{p+1},$

the first equality because $0^p = 0$ for $p \ge 1$ (Integer powers $a^m$ ). Then $(b_n)$ is strictly increasing and unbounded with $b_0 = 0$ and $b_n > 0$ for $n \ge 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 \ge 1$ , where the quotient is defined. For $p = 1$ this is

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

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 \ge 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 \ge 1$ (Integer powers $a^m$ ); $a^{m+n} = a^m a^n$ and $a^{-m} = (a^m)^{-1}$ for $a \ne 0$ (Laws of integer exponents); for $0 \le a < b$ and $n \ge 1$ , $a^n < b^n$ , and $a \ge 1$ with $n \ge 1$ gives $a^n \ge 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 \ge 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 $\mathbb{R}$ and its reciprocal form (Every complete ordered field is Archimedean, For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$ ); 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 \le m < n$ and $p + 1 \ge 1$ , so $m^{p+1} < n^{p+1}$ .

L2L6L8

1.2

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

L2L6L8

1.3

$b_0 = 0^{p+1} = 0$ and $b_n > 0$ for $n \ge 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\big((n+1)^{p+1} - n^{p+1}\big)^{-1}$ .

L2L4

1.5

Put $\tau_n := n\,(n+1)^{-1}$ ; then $1 - \tau_n = (n+1)^{-1}$ , so given a real $\varepsilon > 0$ and a natural $m \ge 1$ with $1/m < \varepsilon$ one has $|\tau_n - 1| = (n+1)^{-1} < \varepsilon$ for all $n \ge m$ , that is $\lim_n \tau_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} = \big((n+1) - n\big)\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 \tau_n^{\,k} = 1$ for every $k$ ; by induction on $p$ , using the sum rule, $\lim_n \sum_{k=0}^{p}\tau_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} = \tau_n^{\,k}$ gives $d_n = \big(\sum_{k=0}^{p}\tau_n^{\,k}\big)^{-1}$ , and $\sum_{k=0}^{p}\tau_n^{\,k} \ge 1 > 0$ for every $n$ , the term at $k = 0$ being $1$ and all terms being $\ge 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}\big(1^p + \dots + n^p\big)n^{-(p+1)} = (p+1)^{-1}$ over the indices $n \ge 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 96 results over 28 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

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 + \dots + n)/n^2 \to 1/2(1+2+⋯+n)/n2→1/2 and (1p+⋯+np)/np+1→1/(p+1)(1^p + \dots + n^p)/n^{p+1} \to 1/(p+1)(1p+⋯+np)/np+1→1/(p+1) for natural ppp