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

For the Dirichlet function every uniform partition with rational tags gives Riemann sum 1, so the sums converge along that sequence of tagged partitions although the function is not integrable: the mesh condition of the Riemann definition quantifies over all tagged partitions and cannot be weakened to one sequence

Statement refuted

Refuted: that a bounded f on [a,b] is Riemann integrable with integral I as soon as there is one sequence (PN,ξN) of tagged partitions with ∥PN∥→0 and S(f,PN,ξN)→I (Tagged partitions of [a,b], with a tag ξi in each subinterval, and the Riemann sum S(f,P,ξ)=∑if(ξi) Δ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).

The witness is again the Dirichlet function on [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). Take PN:=UN, the uniform partition into N≥1 parts, and tag each subinterval by its left endpoint ξiN:=ι(i)/ι(N), a rational. Then

∥UN∥=1ι(N)⟶0,S(1Q,UN,ξN)=1  for every N≥1,

so the Riemann sums converge, to 1; and yet 1Q is not Riemann integrable on [0,1] (The Dirichlet function on [0,1] has lower Darboux integral 0 and upper Darboux integral 1, so it is bounded and not Riemann integrable).

What this shows about The Darboux and Riemann definitions agree: a bounded f on [a,b] is Darboux integrable with integral I if and only if for every real ε>0 there is a real δ>0 such that ∣S(f,P,ξ)−I∣<ε for every tagged partition of mesh below δ. Condition 2 there quantifies over every tagged partition of mesh below δ, tags included, and the quantifier cannot be replaced by the existence of one good sequence. Tagging the very same partition by irrationals instead gives Riemann sum 0, so for each N the two taggings of UN give the two values 1 and 0; no real number is within 1/2 of both.

Facts & Assumptions

Given: g:[0,1]→R with g(x)=1 for rational x and g(x)=0 for irrational x; for N≥1 the uniform partition UN=(N,t) of [0,1] with ti=ι(i)/ι(N) and Δi=1/ι(N); and the tagging ξN with ξiN:=ti for i<N.

[A1]

The refuted claim: if some sequence of tagged partitions of [0,1] has meshes tending to 0 and Riemann sums tending to I, then g is Riemann integrable with integral I.

[L1]

For UN: ti=ι(i)/ι(N)∈[0,1], ti<ti+1, Δi=1/ι(N), ∑i<NΔi=1, and ∥UN∥=1/ι(N) (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).

[L2]

ξiN:=ti∈Ii defines a tagging of UN, and S(g,UN,ξN)=∑i<Ng(ξiN)Δi (Tagged partitions of [a,b], with a tag ξi in each subinterval, and the Riemann sum S(f,P,ξ)=∑if(ξi) Δi).

[L4]

Finite sums: scaling and ∑i<N1⋅Δi=∑i<NΔi (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L5]

A constant sequence converges to its value; and for every real η>0 there is N≥1 with 1/ι(N)<η, so the sequence N↦1/ι(N) converges to 0, its terms being positive and decreasing below every positive bound (Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences, For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε, Every complete ordered field is Archimedean, Canonical naturals are positive and strictly increasing, Basic properties of the absolute value).

[L9]

Ordered-field arithmetic: the order is total and transitive, ι(N)>0 for N≥1, and 0≠1 (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

For each N≥1, (UN,ξN) is a tagged partition of [0,1] of mesh 1/ι(N), by [L1] and [L2].

givenL1L2
1.2

By [L3] every tag ξiN=ti is rational, so g(ξiN)=1; hence by [L2], [L4] and [L1], S(g,UN,ξN)=∑i<N1⋅Δi=∑i<NΔi=1.

givenL1L2L3L4
2.1

The sequence N↦∥UN∥=1/ι(N) converges to 0 and the sequence N↦S(g,UN,ξN) is constantly 1, hence converges to 1, by [L5].

step 1.1step 1.2L5
3.1

So the hypothesis of [A1] is met with I:=1; but g is not Riemann integrable on [0,1] by [L6]. [A1] is therefore refuted.

step 2.1A1L6
4.1

Moreover, for each N≥1 the same partition carries a tagging whose Riemann sum is 0: by [L7] each open interval (ti,ti+1) contains an irrational, and choosing one in each of the N subintervals is a finite selection, giving a tagging ζ of UN with g(ζi)=0 for every i<N and hence S(g,UN,ζ)=0 by [L2] and [L4]. So for every real δ>0 there are tagged partitions of mesh below δ with Riemann sum 1 and others with Riemann sum 0, and by [L9] no single real I can satisfy the condition of [L8] at ε:=2−1.

step 1.1step 1.2L2L4L5L7L8L9∎

Remarks

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