Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-21
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.

F(x)=x2sin(1/x2) has an unbounded derivative whose Henstock–Kurzweil integral is sin1

Example

Define F(0)=0 and F(x)=x2sin(1/x2) for 0<x1. Then F is differentiable on [0,1] and

f(x)=F(x)=2xsin(1/x2)2xcos(1/x2)(x>0),f(0)=0.

F(x)=x2sin(1/x2) has an unbounded derivative whose Henstock–Kurzweil integral is sin1.

The derivative f of x2sin(1/x2) is Henstock–Kurzweil integrable on [0,1].

Facts & Assumptions

Given: The displayed function F and its derivative candidate f.

[L1]

If a<b, F:[a,b]R is differentiable in the domain-relative sense, including at the endpoints, and f=F, then f is Henstock–Kurzweil integrable and abf=F(b)F(a) (Every derivative is Henstock–Kurzweil integrable and satisfies Newton–Leibniz).

[L2]

For every integer m, sin(π/2+2mπ)=1, sin(2mπ)=0, and cos(2mπ)=1 (Quarter-turn values and shifts by pi/2 and pi, The zero sets of sine and cosine and the least positive common period 2 pi).

[L3]

If g is differentiable at x and f is differentiable at g(x), then the chain rule gives (fg)(x)=f(g(x))g(x) (The chain rule, in one line from Carathéodory: if g is differentiable at c and f is differentiable at g(c), then fg is differentiable at c with (fg)(c)=f(g(c))g(c)).

[L5]

Sine and cosine have derivatives cos and sin (The derivatives of sine and cosine are cosine and minus sine).

[L6]

For every real u, sinu1 (Parity and the Pythagorean identity for sine and cosine).

Verification

technique · direct
1.1

Applying [L3], [L4], and [L5] gives the displayed derivative for x>0, while [L6] gives F(x)/x=xsin(1/x2)x0 and hence F(0)=0. For every natural m1, at xm=1/2πm the values in [L2] give f(xm)=2/xm, which is unbounded.

givenL2L3L4L5L6algebra
2.1

Applying [L1] gives HK integrability and 01f=F(1)F(0)=sin1.

step 1.1L1

Depends on

Used by

Dependency tree · two levels

35 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