LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-11

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 Riemann–Stieltjes integral is unique

Statement

For fixed $f, α : [a, b] \to R$ , at most one real number satisfies the mesh-limit condition defining $\int_{a}^{b} f d α$ .

Facts & Assumptions

Given: Two reals $I, J$ satisfying the defining mesh condition for the same functions $f, α$ .

[L1]

The mesh-limit condition quantifies over every sufficiently fine tagged partition (Riemann–Stieltjes sums, upper and lower sums, and the Riemann–Stieltjes integral).

[L2]

Uniform partitions have mesh $(b - a) / N$ for every natural $N \geq 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, The canonical natural $ι (n) = n \cdot 1_{F}$ of a field).

[L3]

Reciprocal naturals become arbitrarily small (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[L4]

$∣ u + v ∣ \leq ∣ u ∣ + ∣ v ∣$ and $∣ u ∣ = 0$ exactly when $u = 0$ (The triangle inequality, Basic properties of the absolute value).

Proof

technique · direct

1.1L1L2L3choose

Given $ε > 0$ , choose positive thresholds $δ_{I}, δ_{J}$ for error $ε / 2$ in the two mesh conditions. By [L3] choose a natural $N \geq 1$ whose uniform partition has mesh smaller than both thresholds, and give it arbitrary tags.

2.1step 1.1L1L4∎

For its sum $S$ , $∣ I - J ∣ \leq ∣ I - S ∣ + ∣ S - J ∣ < ε$ . Since this holds for every $ε > 0$ , $∣ I - J ∣ = 0$ and $I = J$ . The singleton interval has only the prescribed value $0$ .

Depends on

Dependency tree · 2 levels

Sources

William F. Trench, Introduction to Real Analysis, Definition 3.1.5