CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck 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]$ 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] \to R$ be the sign function,

$s (x) : = {\begin{cases} - 1 & - 1 \leq x < 0, \\ 0 & x = 0, \\ 1 & 0 < x \leq 1. \end{cases}$

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

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

Facts & Assumptions

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

[A1]

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

[L1]

A bounded function on $[p, q]$ with at most finitely many discontinuities is Riemann integrable there (A bounded function on $[a, b]$ that is continuous except at finitely many points is Riemann integrable, Lower bound, bounded below, bounded set, The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ , Discontinuity of $f$ at a point of its domain, and its classification: removable discontinuity, jump discontinuity and essential discontinuity, equivalently Rudin's discontinuities of the first and of the second kind).

[L2]

Changing an integrable function at finitely many points changes neither its integrability nor its integral, and $\int_{p}^{q} c = c (q - p)$ for a constant (Changing an integrable function at finitely many points changes neither its integrability nor its integral, If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ ).

[L3]

Additivity, in the oriented form valid for arbitrary points (For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ , claim 3, The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ , The integral function $F (x) : = \int_{a}^{x} f$ of an integrable $f$ ).

[L4]

If $u$ is continuous on an order-convex $I$ and differentiable with $u^{'} = 0$ at every interior point of $I$ , then $u$ is constant on $I$ (A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L5]

A function differentiable at a point is continuous there, and a restriction to a subinterval still having the point as a limit point is differentiable there with the same derivative; every point of a nondegenerate interval is a limit point of it (A function differentiable at $c$ is continuous at $c$ , The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, Limit point, isolated point, adherent point, derived set, and dense subset of $R$ , Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point).

[L6]

If both one-sided limits of a function at $c$ exist and differ, the two-sided limit does not exist (If $c$ is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree, The left and right limits of $f$ at $c$ , as limits of the restrictions of $f$ to $A \cap (- \infty, c)$ and $A \cap (c, \infty)$ , The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).

[L7]

Absolute value: $∣ x ∣ = x$ for $x \geq 0$ and $∣ x ∣ = - x$ for $x \leq 0$ ; $∣ x ∣ / x = 1$ for $x > 0$ and $= - 1$ for $x < 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

$s$ is bounded, with $∣ s ∣ \leq 1$ , and continuous at every point of $[- 1, 1]$ other than $0$ : near a point $x \neq 0$ it is locally constant. So $s$ is integrable on $[- 1, 1]$ , and likewise on $[- 1, 0]$ and on $[0, 1]$ , by [L1].

givenL1

1.2

Assume [A1]. Then $G^{'} = s$ everywhere on $[- 1, 1]$ .

assume-contraA1

2.1

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

step 1.1L2

2.2

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

step 1.2L4L5choose

2.3

On $I_{-} : = [- 1, 0]$ the function $u_{-} (x) : = G (x) + x$ is continuous and differentiable at every $x \in (- 1, 0)$ with $u_{-}^{'} (x) = s (x) + 1 = 0$ ; so $G (x) = - x + c_{2}$ on $[- 1, 0]$ .

step 1.2L4L5choose

3.1

By [L3], $\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) = \int_{- 1}^{x} s$ equals $- 1 + x$ for $x \in [0, 1]$ and equals $- (x - (- 1)) = - x - 1$ for $x \in [- 1, 0]$ , by [L2] applied on the relevant piece; in both cases $F (x) = ∣ x ∣ - 1$ by [L7].

step 2.1L2L3L7

3.3

Evaluating both formulas at $x = 0$ gives $c_{1} = G (0) = c_{2}$ ; write $c$ for the common value, so $G (x) = ∣ x ∣ + c$ for every $x \in [- 1, 1]$ by [L7].

step 2.2step 2.3L7

4.1

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

step 3.3L7

5.1

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

step 4.1A1L6

6.1

Hence no such $G$ exists: $s$ is integrable on $[- 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

Darboux's theorem is not used. The slick argument — a derivative has the intermediate value property, and $s$ does not — rests on Darboux's theorem on the intermediate value property of derivatives. The refutation above uses only A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant and the one-sided limits of a difference quotient, both already published.
The tension with the first fundamental theorem is only apparent. $F$ is differentiable with $F^{'} = s$ at every point of $[- 1, 1]$ except $0$ , which is exactly what The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive promises, since $s$ is continuous exactly off $0$ . What fails is the existence of any function differentiable at $0$ too with derivative $s (0)$ there, and step 4.1 shows the obstruction is the jump of $s$ at $0$ , not a defect of $F$ .
The value $s (0)$ is irrelevant to both halves. Changing it changes neither the integral, by Changing an integrable function at finitely many points changes neither its integrability nor its integral, nor the conclusion of step 5.1, which shows $G$ is not differentiable at $0$ at all and therefore cannot have any prescribed derivative there.

Depends on

Used by

FALSE: for every integrable f on [a,b], the integral function F(x)=∫ₐˣ f satisfies F' = f on [a,b] False statement

Dependency tree · two levels

66 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

Sign function (Wikipedia) (standard reference, not scraped)
Antiderivative (Wikipedia) (standard reference, not scraped)
J. Lebl, Basic Analysis I, Fundamental theorem of calculus (standard reference, not scraped)
Colgate University MATH 323, Chapter 5 notes (standard reference, not scraped)

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