Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
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 nonlinear reparametrisation leaves a Stieltjes integral unchanged

Example

For ϕ(t)=t2\phi(t)=t^2 on [0,1][0,1], the change-of-variable theorem gives the concrete identity ∫01x dx=∫01t2 d(t2)=12.\int_0^1x\,dx=\int_0^1t^2\,d(t^2)=\frac12.

Facts & Assumptions

Given: f(x)=xf(x)=x, α(x)=x\alpha(x)=x, and ϕ(t)=t2\phi(t)=t^2 on [0,1][0,1].

[L1]

Increasing continuous reparametrization preserves a Stieltjes integral (Change of variable for the Riemann–Stieltjes integral).

[L2]

The identity integrator gives the ordinary Riemann integral (The identity integrator recovers the Riemann integral).

[L3]

A C1C^1 integrator reduces the integral to one against its derivative (A continuously differentiable integrator reduces Stieltjes integration to ordinary integration).

Verification

technique · computation
1.1

The map ϕ(t)=t2\phi(t)=t^2 is a strictly increasing continuous bijection of [0,1][0,1] onto itself. Applying [L1] gives ∫01x dx=∫01t2 d(t2)\int_0^1x\,dx=\int_0^1t^2\,d(t^2).

L1
1.2

Direct difference quotients give (t2)′=2t(t^2)'=2t and (t4/2)′=2t3(t^4/2)'=2t^3. Hence [L2], [L3], and the FTC give [L2, L3] ∫01x dx=12,∫01t2 d(t2)=∫012t3 dt=12.\int_0^1x\,dx=\frac12,\qquad \int_0^1t^2\,d(t^2)=\int_0^1 2t^3\,dt=\frac12. ∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 111 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources