Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-08-01
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.

The sign function is Riemann integrable on [1,1][-1,1] and has no primitive there

Statement refuted

False claim: every Riemann integrable function on a closed bounded interval has a primitive there, that is, is the derivative of some function on that interval.

Let s:[1,1]Rs : [-1,1] \to \mathbb{R} be the sign function,

s(x)  :=  {11x<0,0x=0,10<x1.s(x) \;:=\; \begin{cases} -1 & -1 \le x < 0, \\ 0 & x = 0, \\ 1 & 0 < x \le 1. \end{cases}

Then ss is Riemann integrable on [1,1][-1,1] with 11s=0\int_{-1}^{1} s = 0, and there is no G:[1,1]RG : [-1,1] \to \mathbb{R} differentiable at every point of [1,1][-1,1] with G=sG' = s.

The integral function of ss is F(x)=x1F(x) = |x| - 1, which is differentiable at every point of [1,1][-1,1] except x=0x = 0 — exactly the one point where ss is discontinuous. That is consistent with The first fundamental theorem: if ff is integrable on [a,b][a,b] and continuous at cc, then F(c)=f(c)F'(c) = f(c); in particular a continuous ff has FF as a primitive, which claims F(c)=s(c)F'(c) = s(c) only at points of continuity of ss, and it is what the refutation below turns into a contradiction.

Facts & Assumptions

Given: The sign function ss on [1,1][-1,1] and its integral function F(x)=1xsF(x) = \int_{-1}^{x} s.

[A1]

There is G:[1,1]RG : [-1,1] \to \mathbb{R}, differentiable at every point of [1,1][-1,1] as a function on [1,1][-1,1], with G(x)=s(x)G'(x) = s(x) for every x[1,1]x \in [-1,1].

[L7]

Absolute value: x=x|x| = x for x0x \ge 0 and x=x|x| = -x for x0x \le 0; x/x=1|x|/x = 1 for x>0x>0 and =1= -1 for x<0x<0 (Absolute value in an ordered field, Basic properties of the absolute value, Ordered field, Complete ordered field (least-upper-bound property)).

Counterexample

technique · contradiction
1.1

ss is bounded, with s1|s| \le 1, and continuous at every point of [1,1][-1,1] other than 00: near a point x0x \ne 0 it is locally constant. So ss is integrable on [1,1][-1,1], and likewise on [1,0][-1,0] and on [0,1][0,1], by [L1].

givenL1
1.2

Assume [A1]. Then G=sG' = s everywhere on [1,1][-1,1].

assume-contraA1
2.1

On [1,0][-1,0] the function ss agrees with the constant 1-1 except at the single point 00, so 10s=1(0(1))=1\int_{-1}^{0} s = -1\cdot(0-(-1)) = -1 by [L2]; on [0,1][0,1] it agrees with the constant 11 except at 00, so 01s=1\int_0^1 s = 1.

step 1.1L2
2.2

On I+:=[0,1]I_{+} := [0,1] the function u+(x):=G(x)xu_{+}(x) := G(x) - x is continuous, by [L5], and differentiable at every interior point x(0,1)x \in (0,1) with u+(x)=s(x)1=0u_{+}'(x) = s(x) - 1 = 0; so u+u_{+} is constant on [0,1][0,1] by [L4], say G(x)=x+c1G(x) = x + c_1 there.

step 1.2L4L5choose
2.3

On I:=[1,0]I_{-} := [-1,0] the function u(x):=G(x)+xu_{-}(x) := G(x) + x is continuous and differentiable at every x(1,0)x \in (-1,0) with u(x)=s(x)+1=0u_{-}'(x) = s(x)+1 = 0; so G(x)=x+c2G(x) = -x + c_2 on [1,0][-1,0].

step 1.2L4L5choose
3.1

By [L3], 11s=10s+01s=1+1=0\int_{-1}^{1} s = \int_{-1}^{0} s + \int_0^1 s = -1 + 1 = 0.

step 2.1L3
3.2

By [L3] again, F(x)=1xsF(x) = \int_{-1}^{x} s equals 1+x-1 + x for x[0,1]x \in [0,1] and equals (x(1))=x1-(x-(-1)) = -x-1 for x[1,0]x \in [-1,0], by [L2] applied on the relevant piece; in both cases F(x)=x1F(x) = |x| - 1 by [L7].

step 2.1L2L3L7
3.3

Evaluating both formulas at x=0x = 0 gives c1=G(0)=c2c_1 = G(0) = c_2; write cc for the common value, so G(x)=x+cG(x) = |x| + c for every x[1,1]x \in [-1,1] by [L7].

step 2.2step 2.3L7
4.1

The difference quotient of GG at 00 is x(G(x)G(0))/x=x/xx \mapsto (G(x)-G(0))/x = |x|/x, which equals 11 for x>0x > 0 and 1-1 for x<0x < 0 by [L7]; so its right-hand limit at 00 is 11 and its left-hand limit is 1-1.

step 3.3L7
5.1

By [L6] the two-sided limit of that quotient at 00 does not exist, so GG is not differentiable at 00; this contradicts [A1].

step 4.1A1L6
6.1

Hence no such GG exists: ss is integrable on [1,1][-1,1] by step 1.1 and has no primitive there, so the claim is false.

step 1.1step 3.1step 5.1discharge-contradiction

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 117 results over 21 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