Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28
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 nondecreasing f:R→R whose set of discontinuities is exactly Q, obtained from the prescribed-jump construction applied to one fixed enumeration of the rationals

Example

Write Q for the canonical copy of the rationals inside R (The rationals embed densely in the reals). There is a function f:R→R with all of the following properties:

  1. f is nondecreasing (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of R, with the dictionary to monotone sequences) and 0≤f(x)≤1 for every real x;
  2. f is discontinuous at every rational and continuous at every irrational, so its discontinuity set is exactly Q;
  3. every discontinuity of f is a jump (Discontinuity of f at a point of its domain, and its classification: removable discontinuity, jump discontinuity and essential discontinuity, equivalently Rudin's discontinuities of the first and of the second kind).

Explicitly, fixing a bijection e:N→Q (Q is countably infinite), one may take

f(x)  =  ∑k=0∞ak(x),ak(x)={1/2 k+1if e(k)<x,0otherwise,

which is the construction of Converse to Froda: for every at most countable E⊆R there is a bounded nondecreasing f:R→R whose set of discontinuities is exactly E, every one of them a jump applied to E:=Q (Series, partial sums, convergence and the sum, divergence, and the tail series, For ∣r∣<1, ∑k≥0rk=1/(1−r), and for ∣r∣≥1 the series diverges).

This is the extreme case allowed by Froda's theorem. Froda's theorem: the set of discontinuities of a monotone function on an interval is at most countable, the injection into N being built from one fixed enumeration of the rationals by least index, so no choice principle is used says that a monotone function on an interval has at most countably many discontinuities; Q is countable and dense, so the bound is attained by a set that meets every interval. A monotone function can therefore be discontinuous on a dense set, and it is nevertheless continuous on a set whose complement is countable.

Facts & Assumptions

Given: The canonical copy Q⊆R of the rationals.

[L1]

Q≈N, and composing a bijection N→Q with the embedding q↦q^ gives a bijection e:N→Q onto the canonical copy; in particular that copy is nonempty and at most countable (Q is countably infinite, The rationals embed densely in the reals, Finite, countably infinite, countable, uncountable, Equinumerous sets, A≈B and A⪯B, A nonempty set is at most countable iff it is a surjective image of N).

Verification

technique · direct
1.1

Q, as a subset of R, is at most countable.

L1
2.1

Applying the prescribed-discontinuity theorem with E:=Q produces a nondecreasing f:R→R with values in [0,1], continuous at every irrational, discontinuous at every rational, and with every discontinuity a jump. This is exactly claims 1, 2 and 3.

step 1.1L2
3.1

The displayed formula is the function the theorem constructs, for the surjection e of [L1]: the construction there sums the masses 1/2 k+1 over the indices k with e(k)<x.

step 2.1L1L2
4.1

The example is consistent with Froda's theorem and is extremal for it: the discontinuity set Q is at most countable, as Froda requires, and no larger discontinuity set is possible for any monotone function.

step 2.1L1L3∎

Remarks

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

65 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