Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26
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.

A bounded function on a closed bounded interval, or on a closed nondegenerate rectangle, is Riemann integrable exactly when its discontinuity set has Lebesgue measure zero

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)).

  1. Let a<b be reals and let f:[a,b]R be bounded, with discontinuity set D. Then f is Riemann integrable on [a,b] if and only if D is Lebesgue measurable with λ1(D)=0.
  2. Let m1 and let f be a bounded real function on a closed nondegenerate rectangle in Rm, with discontinuity set D. Then f is Riemann integrable if and only if D is Lebesgue measurable with λm(D)=0.

The choice ledger of the cited criteria is inherited, not discharged. In Lebesgue's criterion for Riemann integrability: a bounded f on [a,b] is Riemann integrable if and only if its set of discontinuities has measure zero the implication from integrability to nullity of D uses countable choice and the converse implication is a theorem of ZF; the translation performed here rests on the construction of λ, which uses countable choice in both directions, so the statement above carries the hypothesis throughout.

Facts & Assumptions

Given: The Axiom of Countable Choice, a bounded real function on a closed bounded interval or on a closed nondegenerate rectangle, and its discontinuity set D.

[L1]

Assuming countable choice, λ1(A)=0 if and only if AR has measure zero in the covering sense, and a set of Lebesgue outer measure zero is measurable of measure zero (A subset of R has Lebesgue outer measure zero if and only if it has measure zero in the sense of countable closed-interval covers, Assuming countable choice, L(Rn) is a sigma-algebra containing every elementary set and λn is a complete measure extending elementary volume).

[L2]

Assuming countable choice, λm(E)=0 if and only if ERm is null in the covering sense (A subset of Rm has Lebesgue outer measure zero if and only if it is null in the sense of countable closed-cube covers).

[F1]

Let a<b be reals, let f:[a,b]R be bounded and let D be its set of discontinuities; then f is Riemann integrable on [a,b] if and only if D has measure zero (Lebesgue's criterion for Riemann integrability: a bounded f on [a,b] is Riemann integrable if and only if its set of discontinuities has measure zero, Measure zero (a countable cover by intervals of total length below every ε) and content zero (a finite such cover)).

[F2]

A bounded real function on a closed nondegenerate rectangle in Rm, m1, is Riemann integrable if and only if its discontinuity set is null (Lebesgue's criterion in Rm: a bounded function on a closed nondegenerate rectangle is Riemann integrable iff its discontinuity set is null, Measure zero and content zero in Rm by countable and finite cube covers).

[F3]

A measurable set NA is μ-null if μ(N)=0 (Measure-null sets and almost-everywhere statements relative to a measure).

Proof

technique · direct
1.1

On the line, "D has measure zero" in the covering sense of the cited criterion is equivalent to λ1(D)=0, and a set of Lebesgue outer measure zero is Lebesgue measurable of measure zero, while conversely λ1(D)=0 for a measurable D says λ1(D)=0.

L1F3
1.2

In Rm, "the discontinuity set is null" in the covering sense of the cited criterion is likewise equivalent to λm(D)=0, hence to D being Lebesgue measurable with λm(D)=0.

L1L2F3
2.1

Substituting these equivalences into the two published criteria gives claims 1 and 2.

step 1.1step 1.2F1F2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

81 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