ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

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.

$\int_{0}^{1} x^{2} = 1 / 3$ , computed from the Darboux definition with uniform partitions and the closed form $\sum_{k < n} k^{2} = n (n - 1) (2 n - 1) / 6$

Example

Let $f : [0, 1] \to R$ be $f (x) = x^{2}$ (Integer powers $a^{m}$ ). Then $f$ is Riemann integrable on $[0, 1]$ and

$\int_{0}^{1} x^{2} d x = \frac{1}{3} .$

Everything is computed from the definition. For the uniform partition $U_{N}$ of $[0, 1]$ into $N \geq 1$ parts (Partition of $[a, b]$ as a finite strictly increasing list $a = t_{0} < t_{1} < \dots < t_{n} = b$ , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions) the two Darboux sums (For bounded $f$ on $[a, b]$ and a partition $P$ : the infimum $m_{i}$ and supremum $M_{i}$ of $f$ on the $i$ -th subinterval, and the lower and upper Darboux sums $L (f, P) = \sum_{i} m_{i} Δ_{i}$ and $U (f, P) = \sum_{i} M_{i} Δ_{i}$ ) are

$L (f, U_{N}) = \frac{(N - 1) (2 N - 1)}{6 N^{2}}, U (f, U_{N}) = \frac{(N + 1) (2 N + 1)}{6 N^{2}}, U (f, U_{N}) - L (f, U_{N}) = \frac{1}{N},$

where a natural $N$ multiplying or dividing a real stands for its canonical natural $ι (N)$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field), as in clause 2 of Laws of finite sums and finite products. Both expressions converge to $1 / 3$ as $N$ grows, the lower sums from below and the upper sums from above, and the gap $1 / N$ is what Archimedes' property drives to $0$ .

The arithmetic rests on one closed form, valid for every $n \in N$ :

$6 \sum_{k < n} ι (k)^{2} = ι (n) (ι (n) - 1) (2 ι (n) - 1),$

which at $n = 0$ reads $0 = 0$ and is the familiar $n (n - 1) (2 n - 1) / 6$ written so that the empty sum is the case $n = 0$ rather than an exception. Note the indexing: the sum runs over $k < n$ , so its last term is $ι (n - 1)^{2}$ and not $ι (n)^{2}$ .

Facts & Assumptions

Given: $f : [0, 1] \to R$ with $f (x) = x^{2}$ , and for $N \geq 1$ the uniform partition $U_{N} = (N, t)$ of $[0, 1]$ with $t_{i} = ι (i) / ι (N)$ for $i \leq N$ and lengths $Δ_{i} = 1 / ι (N)$ .

[L1]

For $U_{N}$ : $t_{0} = 0$ , $t_{N} = 1$ , $t_{i} < t_{i + 1}$ , $Δ_{i} = 1 / ι (N)$ for $i < N$ , $\sum_{i < N} Δ_{i} = 1$ , and $I_{i} = [t_{i}, t_{i + 1}]$ (Partition of $[a, b]$ as a finite strictly increasing list $a = t_{0} < t_{1} < \dots < t_{n} = b$ , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L2]

$m_{i} = \inf f [I_{i}]$ , $M_{i} = \sup f [I_{i}]$ , $L (f, P) = \sum_{i < N} m_{i} Δ_{i}$ , $U (f, P) = \sum_{i < N} M_{i} Δ_{i}$ , and $L (f, P) \leq \underline{\int_{0}^{1}} f \leq \overline{\int_{0}^{1}} f \leq U (f, P)$ for every partition $P$ ; when $f$ is integrable, $\int_{0}^{1} f$ is the common value of the two integrals (For bounded $f$ on $[a, b]$ and a partition $P$ : the infimum $m_{i}$ and supremum $M_{i}$ of $f$ on the $i$ -th subinterval, and the lower and upper Darboux sums $L (f, P) = \sum_{i} m_{i} Δ_{i}$ and $U (f, P) = \sum_{i} M_{i} Δ_{i}$ , The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ ).

[L3]

For $0 \leq a < b$ one has $a^{2} < b^{2}$ ; a set with a least element has it as its infimum and one with a greatest element has it as its supremum (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ , Integer powers $a^{m}$ , Greatest lower bound (infimum), Maximum and minimum of a set, Complete ordered field (least-upper-bound property)).

[L4]

The closed form. For every $n \in N$ , $6 \sum_{k < n} ι (k)^{2} = ι (n) (ι (n) - 1) (2 ι (n) - 1)$ . This is an induction on $n$ (The principle of mathematical induction) from the recursion clause $\sum_{k < n + 1} = \sum_{k < n} + ι (n)^{2}$ of Finite sums and finite products, by recursion and the identity $x (x - 1) (2 x - 1) + 6 x^{2} = x (x + 1) (2 x + 1)$ , valid in any commutative ring and in particular for $x = ι (n)$ (Ordered field, Canonical naturals are positive and strictly increasing).

[L5]

Finite sums: scaling, additivity, telescoping $\sum_{i < N} (c_{i + 1} - c_{i}) = c_{N} - c_{0}$ , and $ι (i + 1) = ι (i) + 1$ (Finite sums and finite products, by recursion, Laws of finite sums and finite products, The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing).

[L6]

$x \mapsto x^{2}$ is continuous on $[0, 1]$ , being a polynomial function, and a continuous function on a closed bounded interval with distinct endpoints is Riemann integrable (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point, A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

[L7]

For every real $η > 0$ there is a natural $N \geq 1$ with $1 / ι (N) < η$ , and $ι (N) > 0$ for $N \geq 1$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Every complete ordered field is Archimedean, The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing).

[L8]

Ordered-field arithmetic and the absolute value: adding a constant and multiplying by a positive quantity preserve an inequality; the order is total and transitive; $∣ u - v ∣ \leq w$ whenever $c \leq u \leq d$ , $c \leq v \leq d$ and $d - c \leq w$ (Basic properties of the absolute value, Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication, Ordered field, Complete ordered field (least-upper-bound property)). These order-arithmetic facts are stated by their sources for the strict order only; the nonstrict forms used below follow by adjoining the equality case, in which the two sides coincide.

Verification

technique · direct

1.1

$f$ is continuous on $[0, 1]$ and $0 < 1$ , so $f$ is Riemann integrable on $[0, 1]$ by [L6]; write $J : = \int_{0}^{1} f$ .

givenL6

1.2

On $I_{i} = [t_{i}, t_{i + 1}]$ with $0 \leq t_{i} < t_{i + 1}$ the function $f$ takes its least value at $t_{i}$ and its greatest at $t_{i + 1}$ , by [L3]; both values are attained, so $m_{i} = t_{i}^{2} = ι (i)^{2} / ι (N)^{2}$ and $M_{i} = t_{i + 1}^{2} = ι (i + 1)^{2} / ι (N)^{2}$ by [L3] and [L1].

givenL1L3

2.1

By [L2], [L5] and [L1], $L (f, U_{N}) = \sum_{i < N} \frac{ι (i)^{2}}{ι (N)^{2}} \cdot \frac{1}{ι (N)} = \frac{1}{ι (N)^{3}} \sum_{i < N} ι (i)^{2}$ , and by [L4] this equals $\frac{ι (N) (ι (N) - 1) (2 ι (N) - 1)}{6 ι (N)^{3}} = \frac{(ι (N) - 1) (2 ι (N) - 1)}{6 ι (N)^{2}}$ .

step 1.2L1L2L4L5

2.2

Likewise $U (f, U_{N}) = \frac{1}{ι (N)^{3}} \sum_{i < N} ι (i + 1)^{2}$ . Since $\sum_{i < N} ι (i + 1)^{2} = \sum_{k < N + 1} ι (k)^{2} - ι (0)^{2} = \sum_{k < N + 1} ι (k)^{2}$ by [L5] and $ι (0) = 0$ , [L4] applied at $N + 1$ gives $U (f, U_{N}) = \frac{(ι (N) + 1) (2 ι (N) + 1)}{6 ι (N)^{2}}$ .

step 1.2L1L2L4L5

2.3

Directly, $U (f, U_{N}) - L (f, U_{N}) = \frac{1}{ι (N)^{3}} \sum_{i < N} (ι (i + 1)^{2} - ι (i)^{2}) = \frac{ι (N)^{2} - ι (0)^{2}}{ι (N)^{3}} = \frac{1}{ι (N)}$ , by telescoping in [L5].

step 1.2L1L2L5

3.1

Expanding by [L8], $\frac{1}{3} - L (f, U_{N}) = \frac{3 ι (N) - 1}{6 ι (N)^{2}} > 0$ and $U (f, U_{N}) - \frac{1}{3} = \frac{3 ι (N) + 1}{6 ι (N)^{2}} > 0$ for $N \geq 1$ , so $L (f, U_{N}) < \frac{1}{3} < U (f, U_{N})$ .

step 2.1step 2.2L7L8

3.2

By [L2], $L (f, U_{N}) \leq J \leq U (f, U_{N})$ as well.

step 1.1step 2.1step 2.2L2

4.1

Both $J$ and $1 / 3$ lie in the interval with endpoints $L (f, U_{N})$ and $U (f, U_{N})$ , whose length is $1 / ι (N)$ by step 2.3, so $∣ J - 1 / 3 ∣ \leq 1 / ι (N)$ for every natural $N \geq 1$ , by [L8].

step 2.3step 3.1step 3.2L8

5.1

If $J \neq 1 / 3$ then $∣ J - 1 / 3 ∣ > 0$ , and [L7] supplies $N \geq 1$ with $1 / ι (N) < ∣ J - 1 / 3 ∣$ , contradicting step 4.1. Hence $J = 1 / 3$ , that is $\int_{0}^{1} x^{2} d x = 1 / 3$ .

step 4.1L7L8∎

Remarks

The first index is $0$ and the last term of the lower sum is not $1$ . The lower sum uses $m_{i} = t_{i}^{2}$ with $i$ running from $0$ , so its first term is $0$ and its last is $((N - 1) / N)^{2} \cdot (1 / N)$ ; the upper sum uses $M_{i} = t_{i + 1}^{2}$ and so ends at $1 \cdot (1 / N)$ . Reading the closed form with the other convention, $\sum_{k = 1}^{n} k^{2} = n (n + 1) (2 n + 1) / 6$ , and attaching it to the wrong sum is the standard way to lose the factor and land on $1 / 2$ or $1 / 6$ instead of $1 / 3$ .
The gap is exactly $1 / N$ , not merely $O (1 / N)$ . Step 2.3 computes it by telescoping without evaluating either sum, which is also the cheapest route to integrability through Riemann's criterion: a bounded $f$ on $[a, b]$ is Darboux integrable if and only if for every real $ε > 0$ there is a partition $P$ with $U (f, P) - L (f, P) < ε$ : the continuity of $x^{2}$ is not needed for that, only for the shortcut taken in step 1.1.
What this example does not do. No antiderivative and no fundamental theorem of calculus is used or available at this point in the reading order; the value $1 / 3$ is extracted from the two sums and the Archimedean property alone. The same computation with $x^{3}$ needs $\sum_{k < n} k^{3}$ and is no harder, but it is not carried out here.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

69 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

Riemann integral (Wikipedia) (standard reference, not scraped)
Square pyramidal number (Wikipedia) (standard reference, not scraped)
J. Hunter, Chapter 11: The Riemann Integral (standard reference, not scraped)

∫01x2=1/3∫01​x2=1/3, computed from the Darboux definition with uniform partitions and the closed form ∑k<nk2=n(n−1)(2n−1)/6∑k<n​k2=n(n−1)(2n−1)/6