Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-09-05
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 pure jump function can have dense discontinuities and derivative 0 almost everywhere

Example

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Choose an enumeration (qn)n≥1 of Q∩(0,1] without repetitions and define

J(x):=∑qn≤x2−n,x∈[0,1].

Then J is increasing, it is discontinuous exactly at the rationals in (0,1], those discontinuities are dense in [0,1], and J′(x)=0 almost everywhere.

Facts & Assumptions

Given: Countable Choice and an enumeration (qn) without repetitions of Q∩(0,1].

[A1]

The symbols are those of the statement.

Verification

technique · direct
1.1given

Every summand x↦1{qn≤x}2−n is nondecreasing, so J is nondecreasing. If x<y, choose qm∈Q∩(x,y]; then the mth summand contributes 0 at x and 2−m at y, so J(y)−J(x)≥2−m>0. Hence J is increasing. At a rational point qm, the value of the mth summand jumps by 2−m, so J is discontinuous at qm. Thus the discontinuity set contains Q∩(0,1], hence is dense in [0,1].

2.1step 1.1

Let x∈[0,1) be irrational. Given ε>0, choose N so large that ∑n>N2−n<ε/3. Because x≠qn for n≤N, there is a neighborhood of x containing none of the finitely many rationals q1,…,qN, so the first N partial sums are constant on that neighborhood. The tail contributes less than ε/3 on either side, so J is continuous at x. Also J(0)=0 because every qn is positive. Therefore the discontinuity set is exactly Q∩(0,1].

3.1step 1.1step 2.1

The function J has no endpoint defect at 0, and because the enumeration has no repetitions, at each qn its jump size is exactly 2−n. Therefore claim 2 of A nondecreasing function splits uniquely into a jump part and a continuous part identifies the jump function of J with J itself. Countable Choice is assumed, so the jump-function theorem A jump function has derivative zero almost everywhere gives J′=0 almost everywhere.

4.1step 1.1step 2.1step 3.1∎

Steps 1.1 through 3.1 prove the example.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

30 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