Alphabeta Math
CounterexampleConstruction: 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.

The Dirichlet function on [0,1] has lower Darboux integral 0 and upper Darboux integral 1, so it is bounded and not Riemann integrable

Statement refuted

Refuted: that every bounded function on a closed bounded interval with distinct endpoints is Riemann integrable (FALSE: every bounded function on [a,b] is Riemann integrable, The lower and upper Darboux integrals of a bounded f on [a,b] as sup⁡PL(f,P) and inf⁡PU(f,P), Darboux integrability as their equality, and the notation ∫abf).

The witness is the Dirichlet function 1Q restricted to [0,1] (The Dirichlet function 1Q, and Thomae's function t with t(x)=1/q at a rational x=p/q in lowest terms with q≥1 and t(x)=0 at every irrational x). It takes only the values 0 and 1, so it is bounded (Lower bound, bounded below, bounded set); every lower Darboux sum is 0 and every upper Darboux sum is 1; hence

∫01‾1Q  =  0  ≠  1  =  ∫01‾1Q,

and the function is not Riemann integrable. The two Darboux integrals are as far apart as the range of the function allows.

Facts & Assumptions

[A1]

The refuted claim: every bounded function on such an interval is Riemann integrable (FALSE: every bounded function on [a,b] is Riemann integrable).

[L2]

For a partition P=(n,t) of [0,1]: n≥1, ti<ti+1, Δi>0, ∑i<nΔi=1, Ii=[ti,ti+1], and (ti,ti+1) is a nonempty open interval contained in Ii (Partition of [a,b] as a finite strictly increasing list a=t0<t1<⋯<tn=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).

[L3]

mi=inf⁡g[Ii], Mi=sup⁡g[Ii], L(g,P)=∑i<nmiΔi, U(g,P)=∑i<nMiΔi; ∫01‾g is the supremum of the lower sums and ∫01‾g the infimum of the upper sums; g is integrable exactly when they agree (For bounded f on [a,b] and a partition P: the infimum mi and supremum Mi of f on the i-th subinterval, and the lower and upper Darboux sums L(f,P)=∑imiΔi and U(f,P)=∑iMiΔi, The lower and upper Darboux integrals of a bounded f on [a,b] as sup⁡PL(f,P) and inf⁡PU(f,P), Darboux integrability as their equality, and the notation ∫abf).

[L4]

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

[L5]
[L6]

Ordered-field arithmetic: 0≠1, and the order is total and transitive (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.

Counterexample

technique · direct
1.1

g is bounded, with 0≤g(x)≤1 for every x∈[0,1], so its Darboux sums and integrals are defined by [L3].

givenL3
1.2

Let P=(n,t) be any partition of [0,1] and i<n. By [L2] the interval (ti,ti+1) is nonempty and open, so by [L1] it contains a rational and an irrational, both lying in Ii. Hence g[Ii]={0,1} and, by [L4], mi=0 and Mi=1.

givenL1L2L4
2.1

Therefore L(g,P)=∑i<n0⋅Δi=0 and U(g,P)=∑i<n1⋅Δi=∑i<nΔi=1, for every partition P of [0,1], by [L3], [L5] and [L2].

step 1.2L2L3L5
3.1

The set of lower sums is {0} and the set of upper sums is {1}, so ∫01‾g=0 and ∫01‾g=1 by [L4] and [L3]. Since 0≠1 by [L6], g is not Riemann integrable on [0,1].

step 2.1L3L4L6
4.1

So g is bounded on [0,1], an interval with 0<1, and is not Riemann integrable: [A1] is refuted.

step 1.1step 3.1A1∎

Remarks

Depends on

Used by

Dependency tree · two levels

62 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