Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14
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.

Borel's exceptional set can be uncountable and null

Example

Assume the Axiom of Countable Choice. Let C be the set of points in [0,1) whose canonical binary expansions have digit zero at every even position. Then C is uncountable and Lebesgue null, and no member of C is normal in base two.

Facts & Assumptions

Given: Countable choice and the set C just defined.

[F1]

Canonical digit strings are not eventually one, and length-q digit cylinders are half-open dyadic intervals (Canonical base-b expansions and normal numbers, Base-b digit cylinders are orbit cylinders).

[F2]

A decreasing sequence of finite-measure sets has intersection measure equal to the infimum of its measures (Continuity from above when one set has finite measure), and half-open intervals have their stated lengths (A box in Rn with parameters ai≤bi is Lebesgue measurable of measure ∏i<n(bi−ai), whichever of its faces are included).

[F3]

There is no surjection from N onto its power set (Cantor's theorem: A≺P(A)); a nonempty set is countable exactly when it is a surjective image of N (A nonempty set is at most countable iff it is a surjective image of N).

[F4]

Almost every point is normal, but this theorem asserts nullity rather than countability of the exceptional set (Borel's normal number theorem).

Verification

technique · constructive
1.1F1F2algebra

Let Cn require only digits 2,4,…,2n to be zero. Prescribing the first 2n digits leaves n odd-position digits free, so [F1] writes Cn as a disjoint union of 2n half-open cylinders, each of length 2−2n. Consequently λ(Cn)=2−n.

1.2F1construct

For A⊆N>0, form the binary string whose digit at position 2r−1 is 1 exactly when r∈A, and whose even-position digits are all 0. Its series xA=∑r∈A2−(2r−1) lies in [0,1). After any place its tail has a forced zero, so the tail value is strictly less than 1; the greedy recurrence therefore recovers exactly this string. Thus A↦xA maps P(N>0) into C.

1.3F1algebra

Every string in C has every even digit zero, so two adjacent digits can never both equal one. The word 11 has frequency 0, not the required 1/4; hence no member of C is normal in base two.

2.1F2step 1.1

The sets Cn decrease and C=⋂n≥1Cn. Since λ(C1)<∞, continuity from above gives λ(C)=inf⁡n2−n=0.

2.2F1step 1.2

Different subsets have different first differing odd digit, so canonical uniqueness makes the map injective. Conversely, the set of odd positions at which a point of C has digit one recovers it, so the map is a bijection onto C.

3.1F3step 2.2

If C were countable, [F3] would give a surjection N→C. Composing it with the inverse bijection in step 2.2 and the explicit shift bijection between N and N>0 would give a surjection N>0→P(N>0), contradicting Cantor's theorem. Hence C is uncountable.

4.1F4step 2.1step 3.1step 1.3discharge-construct∎

Steps 1.3, 2.1, and 3.1 give an uncountable null subset of the exceptional set in [F4]. Countable choice is inherited from the Lebesgue/cylinder suppliers; the family and the coding map are explicit.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

45 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