Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27
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 countable union of measure-zero sets has measure zero, by countable choice

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω\mathrm{AC}_\omega)). Let (An)nN(A_n)_{n \in \mathbb{N}} be a sequence of subsets of R\mathbb{R}, each of measure zero (Measure zero (a countable cover by intervals of total length below every ε\varepsilon) and content zero (a finite such cover)). Then

nNAnhas measure zero.\bigcup_{n \in \mathbb{N}} A_n \quad \text{has measure zero.}

By the padding convention of Measure zero (a countable cover by intervals of total length below every ε\varepsilon) and content zero (a finite such cover) and Finite, countably infinite, countable, uncountable the same conclusion covers the union of an at most countable family of null sets, a finite family being extended by copies of \varnothing.

The hypothesis ACω\mathrm{AC}_\omega is spent at exactly one step, step 2.1 below, where one covering sequence is selected for every AnA_n at once. Each AnA_n has many such covers and nullity provides no rule for singling one out. Nothing else in the proof selects anything: the diagonal enumeration and the estimate are formulas.

Facts & Assumptions

Given: A sequence (An)nN(A_n)_{n \in \mathbb{N}} of null subsets of R\mathbb{R} and a real ε>0\varepsilon > 0. Throughout, θ:=21\theta := 2^{-1}.

[A1]

The Axiom of Countable Choice: every family (Xn)nN(X_n)_{n \in \mathbb{N}} of nonempty sets has a function ff on N\mathbb{N} with f(n)Xnf(n) \in X_n for every nn (The Axiom of Countable Choice (ACω\mathrm{AC}_\omega)).

[L1]

AA is null when for every real η>0\eta > 0 there are sequences (ak)(a_k), (bk)(b_k) with akbka_k \le b_k, Ak[ak,bk]A \subseteq \bigcup_k[a_k,b_k] and k<n(bkak)η\sum_{k<n}(b_k - a_k) \le \eta for every nn (Measure zero (a countable cover by intervals of total length below every ε\varepsilon) and content zero (a finite such cover)).

[L2]

There is a bijection J:N×NNJ : \mathbb{N} \times \mathbb{N} \to \mathbb{N}, with inverse J1J^{-1} (N×NN\mathbb{N} \times \mathbb{N} \approx \mathbb{N}, Injection, surjection, bijection).

[L3]

Powers and the geometric series: θ0=1\theta^0 = 1, θm+1=θmθ\theta^{m+1} = \theta^m \theta, θm>0\theta^m > 0, and m=0θm=2\sum_{m=0}^{\infty}\theta^m = 2 for θ=21\theta = 2^{-1}; a series of nonnegative terms has all its partial sums at most its sum (Integer powers ama^m, For r<1|r| < 1, k0rk=1/(1r)\sum_{k \ge 0} r^k = 1/(1-r), and for r1|r| \ge 1 the series diverges, Series, partial sums, convergence and the sum, divergence, and the tail series, A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum).

[L4]

Finite sums: additivity, scaling, splitting and monotonicity in the terms; a sum of nonnegative terms is nonnegative and does not decrease when further nonnegative terms are adjoined, so a sum of finitely many nonnegative terms indexed injectively inside a finite rectangle is at most the sum over the whole rectangle (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L5]

Every finite list of naturals has an upper bound in N\mathbb{N}, by induction on its length and the totality of the order of N\mathbb{N} (The principle of mathematical induction, Trichotomy of the order on N\mathbb{N}, Order on the natural numbers).

[L6]

Ordered-field arithmetic: 0<10 < 1, so 2>02 > 0 and t21>0t \cdot 2^{-1} > 0 for t>0t > 0; adding a constant and multiplying by a positive preserve an inequality (The multiplicative identity is positive, 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.

Proof

technique · direct
1.1

Let the real ε>0\varepsilon > 0 be given and put εn:=εθn+1\varepsilon_n := \varepsilon \cdot \theta^{n+1} for nNn \in \mathbb{N}, a positive real by [L3] and [L6]. Let XnX_n be the set of all pairs of sequences ((ak),(bk))\big((a_k),(b_k)\big) with akbka_k \le b_k for every kk, Ank[ak,bk]A_n \subseteq \bigcup_k [a_k,b_k] and k<i(bkak)εn\sum_{k<i}(b_k - a_k) \le \varepsilon_n for every iNi \in \mathbb{N}. Each AnA_n is null, so each XnX_n is nonempty by [L1].

givenL1L3L6
2.1

By [A1] fix ff with f(n)Xnf(n) \in X_n for every nn, and write f(n)=((akn)k,(bkn)k)f(n) = \big((a^n_k)_k, (b^n_k)_k\big). This is the one and only application of countable choice in the proof.

step 1.1A1choose
3.1

By [L2] fix a bijection J:N×NNJ : \mathbb{N} \times \mathbb{N} \to \mathbb{N} and define sequences (cj)(c_j) and (dj)(d_j) by cJ(m,k):=akmc_{J(m,k)} := a^m_k and dJ(m,k):=bkmd_{J(m,k)} := b^m_k, which is a total definition because JJ is a bijection; then cjdjc_j \le d_j for every jj. Every xnAnx \in \bigcup_n A_n lies in some AmA_m, hence in some [akm,bkm]=[cJ(m,k),dJ(m,k)][a^m_k, b^m_k] = [c_{J(m,k)}, d_{J(m,k)}] by step 2.1, so nAnj[cj,dj]\bigcup_n A_n \subseteq \bigcup_j [c_j, d_j].

step 2.1L2
4.1

Fix iNi \in \mathbb{N}. The pairs J1(j)J^{-1}(j) for j<ij < i are finitely many and pairwise distinct, so by [L5] there is NNN \in \mathbb{N} with both coordinates of each of them at most NN; since all the terms djcjd_j - c_j are nonnegative, [L4] gives j<i(djcj)mN(kN(bkmakm))\sum_{j<i}(d_j - c_j) \le \sum_{m \le N}\Big(\sum_{k \le N}(b^m_k - a^m_k)\Big). For each mNm \le N the inner sum is k<N+1(bkmakm)εm\sum_{k < N+1}(b^m_k - a^m_k) \le \varepsilon_m by step 2.1, so the whole is at most mNεθm+1=εθm<N+1θmε212=ε\sum_{m \le N} \varepsilon \cdot \theta^{m+1} = \varepsilon \cdot \theta \sum_{m<N+1}\theta^{m} \le \varepsilon \cdot 2^{-1} \cdot 2 = \varepsilon, by [L3], [L4] and [L6].

step 3.1L3L4L5L6
5.1

Steps 3.1 and 4.1 exhibit, for the given ε>0\varepsilon > 0, sequences of closed intervals covering nAn\bigcup_n A_n with every partial total length at most ε\varepsilon; since ε>0\varepsilon > 0 was arbitrary, [L1] gives that nAn\bigcup_n A_n has measure zero.

step 1.1step 3.1step 4.1L1

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 127 results over 31 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources