ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06

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.

Change of variables through an increasing AC map with a positive-measure flat set

Example

Assume the Axioms of Countable Choice and Dependent Choice. Let $E \subset [0, 1]$ be a fat Cantor set with $λ (E) = 1 / 2$ , put $g (x) = \int_{0}^{x} 1_{[0, 1] ∖ E} (t) d t$ , and take $f (y) = 2 y$ . Then $g$ is increasing AC, $g^{'} = 0$ almost everywhere on the positive-measure set $E$ , and $\int_{0}^{1 / 2} 2 y d y = \int_{0}^{1} 2 g (x) g^{'} (x) d x = 1 / 4.$

Facts & Assumptions

Given: Countable choice, dependent choice, the displayed measurable set $E$ , its integral function $g$ , and $f (y) = 2 y$ .

Verification

technique · direct

1.1

The integrand $1_{[0, 1] ∖ E}$ lies in $L^{1} [0, 1]$ . Thus The indefinite integral of an $L^{1}$ function is absolutely continuous makes $g$ AC, and The indefinite integral of an $L^{1}$ function is differentiable almost everywhere gives $g^{'} = 1_{[0, 1] ∖ E}$ a.e.; hence $g^{'} = 0$ on $E$ a.e. and $g (1) = 1 / 2$ .

given

2.1

The hypotheses of Change of variables for an increasing absolutely continuous function hold for $g$ and $f$ .

step 1.1

3.1

Its formula gives the displayed equality, while direct integration gives its common value $1 / 4$ .

step 2.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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

R. K. Srivastava, MA550 Measure Theory Lecture Notes, §4.16 (standard reference, not scraped)