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.

Thomae's function is Riemann integrable on $[0, 1]$ with integral $0$ : it is continuous at every irrational, so its discontinuity set is countable, and every lower Darboux sum is $0$

Example

Let $t : [0, 1] \to R$ be Thomae's function restricted to $[0, 1]$ : at a rational $x$ with least denominator $q (x) \geq 1$ it takes the value $1 / ι (q (x))$ , and at an irrational $x$ the value $0$ (The Dirichlet function $1_{Q}$ , and Thomae's function $t$ with $t (x) = 1 / q$ at a rational $x = p / q$ in lowest terms with $q \geq 1$ and $t (x) = 0$ at every irrational $x$ , The canonical natural $ι (n) = n \cdot 1_{F}$ of a field). Then $t$ is Riemann integrable on $[0, 1]$ and

$\int_{0}^{1} t = 0.$

Two ingredients, and they pull in opposite directions. $t$ is continuous at every irrational and discontinuous at every rational (The Dirichlet function is continuous at no point of $R$ , and Thomae's function is continuous at every irrational and at no rational, so its set of continuity points is exactly the set of irrationals and its oscillation at $c$ equals $t (c)$ ), so its discontinuity set is $Q \cap [0, 1]$ , which is infinite and dense — and countable, which is what A bounded function on $[a, b]$ whose set of discontinuities is at most countable is Riemann integrable needs. The value is then read off the lower sums, every one of which is $0$ because every subinterval contains an irrational (Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $R$ is uncountable).

Every upper sum, by contrast, is strictly positive, since every subinterval contains a rational; the upper integral is nevertheless $0$ , an infimum of positive numbers.

Facts & Assumptions

Given: Thomae's function $t : [0, 1] \to R$ as above.

[L1]

$t (x) = 1 / ι (q (x))$ with $ι (q (x)) \geq 1 > 0$ at a rational $x$ , and $t (x) = 0$ at an irrational $x$ ; hence $0 \leq t (x) \leq 1$ everywhere and $t (x) > 0$ at every rational $x$ (The Dirichlet function $1_{Q}$ , and Thomae's function $t$ with $t (x) = 1 / q$ at a rational $x = p / q$ in lowest terms with $q \geq 1$ and $t (x) = 0$ at every irrational $x$ , The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing).

[L2]

Thomae's function on $R$ is continuous at every irrational and discontinuous at every rational (The Dirichlet function is continuous at no point of $R$ , and Thomae's function is continuous at every irrational and at no rational, so its set of continuity points is exactly the set of irrationals and its oscillation at $c$ equals $t (c)$ ); a restriction is continuous at every point of the smaller domain at which the original is continuous, the same $δ$ serving a condition quantified over fewer points (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).

[L3]

$Q$ is countably infinite and every subset of an at most countable set is at most countable ( $Q$ is countably infinite, Every subset of an at most countable set is at most countable, Finite, countably infinite, countable, uncountable).

[L4]

A bounded function on $[a, b]$ with $a < b$ whose set of discontinuities is at most countable is Riemann integrable (A bounded function on $[a, b]$ whose set of discontinuities is at most countable is Riemann integrable, Lower bound, bounded below, bounded set).

[L5]

The irrationals are dense in $R$ , so every nonempty open interval contains an irrational (Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $R$ is uncountable, The closure equals the set together with its limit points, equals the set of points every neighbourhood of which meets it, and is the smallest closed superset; a set is closed iff it contains its limit points, Interior, closure, boundary and exterior of a subset of $R$ , The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ).

[L6]

For a partition $P = (n, s)$ of $[0, 1]$ : $n \geq 1$ , $s_{i} < s_{i + 1}$ , $Δ_{i} > 0$ , $I_{i} = [s_{i}, s_{i + 1}] \subseteq [0, 1]$ , and $(s_{i}, s_{i + 1})$ is a nonempty open interval (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).

[L7]

$m_{i} = \inf t [I_{i}]$ , $L (t, P) = \sum_{i < n} m_{i} Δ_{i}$ , $\underline{\int_{0}^{1}} t$ is the supremum of the lower sums and $\overline{\int_{0}^{1}} t$ the infimum of the upper sums, and the integral is their common value when they agree (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$ ).

[L8]

A set with a least element has it as its infimum; the supremum of ${0}$ is $0$ (Greatest lower bound (infimum), Maximum and minimum of a set, Complete ordered field (least-upper-bound property)).

[L9]

Finite sums: $\sum_{i < n} 0 = 0$ (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L10]

Ordered-field arithmetic: the order is total and transitive, and a reciprocal of a positive quantity is positive (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

$t$ is bounded on $[0, 1]$ , with $0 \leq t (x) \leq 1$ for every $x$ , by [L1].

givenL1L10

1.2

By [L2], $t$ is continuous at every irrational point of $[0, 1]$ , so its set of discontinuities in $[0, 1]$ is contained in $Q \cap [0, 1]$ , which is at most countable by [L3]; a subset of it is then at most countable as well.

givenL2L3

2.1

By [L4] applied on $[0, 1]$ , with $0 < 1$ , $t$ is Riemann integrable on $[0, 1]$ .

step 1.1step 1.2L4

2.2

Every lower sum is $0$ . Let $P = (n, s)$ be a partition of $[0, 1]$ and $i < n$ . By [L6] the interval $(s_{i}, s_{i + 1})$ is nonempty and open, so by [L5] it contains an irrational $y$ , and $y \in I_{i} \subseteq [0, 1]$ , so $t (y) = 0$ by [L1]. Since $t \geq 0$ by [L1], the value $0$ is the least element of $t [I_{i}]$ and $m_{i} = 0$ by [L8]. Hence $L (t, P) = 0$ by [L7] and [L9].

step 1.1L1L5L6L7L8L9

3.1

The set of lower sums is therefore ${0}$ and $\underline{\int_{0}^{1}} t = 0$ by [L8]; since $t$ is integrable by step 2.1, $\int_{0}^{1} t = 0$ by [L7].

step 2.1step 2.2L7L8∎

Remarks

The discontinuity set is dense and the function is still integrable. $Q \cap [0, 1]$ meets every subinterval of $[0, 1]$ , so no partition isolates the bad points; what saves the function is that the set is countable, hence null (Every at most countable subset of $R$ has measure zero). This is the cleanest witness that "small" for integrability means small in measure and not small in category or in closure.
The same function refutes a plausible converse. $t$ is nonnegative, integrable with integral $0$ , and positive at every rational, so a vanishing integral does not force a nonnegative integrand to vanish (Thomae's function is nonnegative, Riemann integrable on $[0, 1]$ with integral $0$ , and nonzero at every rational, so a vanishing integral does not force a nonnegative integrand to vanish, FALSE: a nonnegative Riemann integrable function on $[a, b]$ with $\int_{a}^{b} f = 0$ is identically zero).
Contrast with the Dirichlet function. $1_{Q}$ is discontinuous everywhere and not integrable (The Dirichlet function on $[0, 1]$ has lower Darboux integral $0$ and upper Darboux integral $1$ , so it is bounded and not Riemann integrable), yet it is nonzero at exactly the same points as $t$ . Only the values differ, and they differ in a way that makes $t$ continuous at every irrational; that is the whole of the difference.

Depends on

Used by

Thomae's function is nonnegative, Riemann integrable on [0,1] with integral 0, and nonzero at every rational, so a vanishing integral does not force a nonnegative integrand to vanish Counterexample

Dependency tree · two levels

91 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

Thomae's function (Wikipedia) (standard reference, not scraped)
Riemann integral (Wikipedia) (standard reference, not scraped)
MAT 125B Discussion 3 (UC Davis) (standard reference, not scraped)
J. Hunter, Chapter 11: The Riemann Integral (standard reference, not scraped)

Thomae's function is Riemann integrable on [0,1][0,1] with integral 00: it is continuous at every irrational, so its discontinuity set is countable, and every lower Darboux sum is 00