Alphabeta Math
False statementConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-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.

FALSE: every nondecreasing function defines a Lebesgue-Stieltjes measure on Borel sets

Statement

False claim. Every nondecreasing function F:R→R defines a Borel measure satisfying μ((a,b])=F(b)−F(a). The valid construction on this page also requires the right-continuity recorded in This page uses the nondecreasing, right-continuous, (a,b]-interval convention.

Facts & Assumptions

Given: The function

F(x):={0,x≤0,1,x>0.

[L1]

Measures are continuous from above on decreasing measurable sets when one set in the chain has finite measure. (Continuity from above when one set has finite measure)

Refutation

technique · direct
1.1

The function F is nondecreasing but not right-continuous at 0: one has F(0)=0 while F(x)=1 for every x>0.

given

If a Borel measure μ satisfied μ((a,b])=F(b)−F(a) for every a<b, then

μ((0,1/n])=F(1/n)−F(0)=1

for every n≥1. [given]

2.1

The sets (0,1/n] decrease to ∅, and μ((0,1])=F(1)−F(0)=1<+∞.

step 1.1L1

Therefore [L1] would force

μ((0,1/n])→μ ⁣(⋂n=1∞(0,1/n])=μ(∅)=0,

contradicting step 1.1. So no such measure exists. [step 1.1, L1] ∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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