What this page costs in choice: Riemann's criterion, the Darboux-Riemann equivalence and integrability of a monotone function are theorems of ZF; integrability of a continuous function inherits the single use of countable choice inside Heine-Cantor; and only the forward half of the Lebesgue criterion spends countable choice, once, at the countable union of null sets

This page develops the Riemann integral over ZF except at the points recorded below. The only choice principle that appears anywhere on it is the Axiom of Countable Choice (The Axiom of Countable Choice ($\mathrm{AC}_\omega$)); the full Axiom of Choice is never used, and no claim is made anywhere that a use recorded here is necessary.

Selecting a tag in every subinterval is not countable choice. 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 $\varepsilon > 0$ there is a real $\delta > 0$ such that $|S(f,P,\xi) - I| < \varepsilon$ for every tagged partition of mesh below $\delta$ picks, for a single fixed partition, one point in each of its $n$ subintervals subject to a supremum condition. That family is listed by the index $i < n$, and a family of nonempty sets listed by a natural number has a choice function outright, by Every natural-number-indexed list of nonempty sets has a choice function on its family of values, which is a theorem of ZF proved by induction. (That lemma is careful to state only the listed form, since no definition of finiteness is available where it is proved; the listed form is what is used here.) The temptation to read this as a choice principle comes from the phrase "for each $i$ pick a point"; the number of picks is what matters, and it is finite.

"For each $n$ pick a partition" would be countable choice, and the page never does it. Both directions of Riemann's criterion: a bounded $f$ on $[a,b]$ is Darboux integrable if and only if for every real $\varepsilon > 0$ there is a partition $P$ with $U(f,P) - L(f,P) < \varepsilon$ and the whole of 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 $\varepsilon > 0$ there is a real $\delta > 0$ such that $|S(f,P,\xi) - I| < \varepsilon$ for every tagged partition of mesh below $\delta$ instantiate an existential a fixed, finite number of times, once per $\varepsilon$ under consideration; no proof on this page ever forms a sequence of partitions indexed by $\mathbb{N}$ and reasons about it. The one place where a sequence of sets does appear is step 7.1 of 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, and that is exactly where the ledger records a cost.

Only the forward half of 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 costs anything. The implication "integrable $\Rightarrow$ the discontinuity set is null" exhibits that set as $\bigcup_k E_{1/(k+1)}$ and applies A countable union of measure-zero sets has measure zero, by countable choice, which assumes $\mathrm{AC}_\omega$ and names its own single use. The converse, "null $\Rightarrow$ integrable", is a theorem of ZF: For every real $\varepsilon > 0$ the set $\{\,x \in A : \omega_f(x) \ge \varepsilon\,\}$ is the intersection with $A$ of a closed subset of $\mathbb{R}$; in particular it is closed in $\mathbb{R}$ when $A = \mathbb{R}$ and A subset of $\mathbb{R}$ is compact if and only if it is closed and bounded are choice-free, For a compact subset of $\mathbb{R}$, measure zero and content zero coincide and A set of content zero has measure zero are choice-free, and the partition is built by Cousin's supremum construction, which uses the completeness of $\mathbb{R}$ and nothing else. This asymmetry is why A bounded function on $[a,b]$ whose set of discontinuities is at most countable is Riemann integrable appears in the table with no cost at all: it uses the converse half only, together with Every at most countable subset of $\mathbb{R}$ has measure zero, whose own statement records that no choice principle is used there.

Heine-Cantor is the page's other source, and it is a single use. Heine-Cantor in $\mathbb{R}$: a continuous real function on a compact subset of $\mathbb{R}$ is uniformly continuous, proved $\mathbb{R}$-natively from sequential compactness states that its proof invokes $\mathrm{AC}_\omega$ exactly once, to select one bad pair of points from each of countably many nonempty sets, and that the implication it borrows from A subset of $\mathbb{R}$ is compact iff it is sequentially compact — compact implies sequentially compact — spends nothing. So A continuous function on $[a,b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion and A bounded function on $[a,b]$ that is continuous except at finitely many points is Riemann integrable each inherit that one use and add none of their own. The neighbouring ledger for the same expenditure on the continuity page is The sequence-to-$\varepsilon$ direction of the Heine criterion uses countable choice for $\mathbb{R}$, and where this library records that cost.

Nothing here says that $\mathrm{AC}_\omega$ is necessary for any of the three theorems that use it. The independence questions for the Heine-Cantor theorem and for the countable additivity of nullity over $\mathbb{R}$ are not settled in this library, and no item on this page asserts anything about them. What the table records is what the proofs on disk actually spend, and it is meant to be checked against them rather than believed.

The one further caution is that a later proof of a result stated here could spend less. The direct argument for A monotone function on $[a,b]$ is Riemann integrable: for the uniform partition into $N$ parts the upper minus lower sum telescopes to $|f(b) - f(a)|\,(b-a)/\iota(N)$ is kept alongside the shorter route through A bounded function on $[a,b]$ whose set of discontinuities is at most countable is Riemann integrable precisely for that reason: the direct one is elementary and quantitative, and both are choice-free, so nothing is lost by keeping the pair.