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.

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

Statement refuted

Refuted: that a nonnegative Riemann integrable function on [a,b] with ∫abf=0 vanishes identically (FALSE: a nonnegative Riemann integrable function on [a,b] with ∫abf=0 is identically zero, 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 Thomae's function t 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). It satisfies 0≤t≤1, it is Riemann integrable with ∫01t=0 (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), and it is positive at every rational point of [0,1] — a dense set, and an infinite one. So the failure is not at a single stray point: the function is nonzero on a dense subset of the interval and the integral still vanishes.

The repaired statement asks for continuity. With f continuous the conclusion is true, and the reason is exactly what fails here: a continuous function positive at one point is positive on a whole subinterval, whereas t is positive only on a set that contains no interval (Both Q and R∖Q are dense in R, and every nonempty open subset of R is uncountable). That repaired statement is not proved here, since the additivity of the integral over subintervals is not available at this point in the reading order.

Facts & Assumptions

Given: Thomae's function t:[0,1]→R, with t(x)=1/ι(q(x)) at a rational x of least denominator q(x)≥1 and t(x)=0 at an irrational x (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, The canonical natural ι(n)=n⋅1F of a field).

[A1]

The refuted claim: a nonnegative Riemann integrable function on a closed bounded interval with distinct endpoints whose integral is 0 vanishes identically.

[L4]

Q is dense in R, so every nonempty open interval contains a rational (Both Q and R∖Q are dense in R, and every nonempty open subset of R is uncountable).

[L5]

Ordered-field arithmetic: 0<2−1<1, so 2−1 lies in [0,1] and is rational; 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), Intervals of R: the nine order-convex forms, nondegeneracy, and length). 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

t is nonnegative on [0,1] by [L1], and it is Riemann integrable there with ∫01t=0 by [L2]; the interval [0,1] has 0<1 by [L5].

givenL1L2L5
1.2

t does not vanish identically: 2−1 is a rational point of [0,1] by [L5], so t(2−1)>0 by [L1].

givenL1L5
2.1

The hypotheses of [A1] hold for t on [0,1] and its conclusion fails, so [A1] is refuted.

step 1.1step 1.2A1
3.1

The failure is dense, not isolated: by [L4] every nonempty open subinterval of [0,1] contains a rational, at which t is positive by [L1]; so { x∈[0,1]:t(x)>0 } meets every subinterval of [0,1] with distinct endpoints. It is also exactly the set of discontinuities of t, by [L3] and [L1].

step 1.2L1L3L4∎

Remarks

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

59 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