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 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 be the sign function,
Then is Riemann integrable on with , and there is no differentiable at every point of with .
The integral function of is , which is differentiable at every point of except — exactly the one point where is discontinuous. That is consistent with The first fundamental theorem: if is integrable on and continuous at , then ; in particular a continuous has as a primitive, which claims only at points of continuity of , and it is what the refutation below turns into a contradiction.
Facts & Assumptions
Given: The sign function on and its integral function .
There is , differentiable at every point of as a function on , with for every .
A bounded function on with at most finitely many discontinuities is Riemann integrable there (A bounded function on 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 on as and , Darboux integrability as their equality, and the notation , Discontinuity at a domain point: removable, jump and essential cases, and the first- and second-kind grouping).
Changing an integrable function at finitely many points changes neither its integrability nor its integral, and for a constant (Changing an integrable function at finitely many points changes neither its integrability nor its integral, If on then for every partition ; in particular every constant function is integrable, with ).
Additivity, in the oriented form valid for arbitrary points (For : is integrable on if and only if it is integrable on and on , and then ; with the oriented form for arbitrary , claim 3, The integral with oriented limits: and , The integral function of an integrable ).
If is continuous on an order-convex and differentiable with at every interior point of , then is constant on (A function continuous on an interval whose derivative vanishes at every interior point of is constant on ; consequently two such functions with the same derivative differ by a constant, Intervals of : the nine order-convex forms, nondegeneracy, and length).
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 is continuous at , The derivative of at a point that is a limit point of , and differentiability on a set, Limit point, isolated point, adherent point, derived set, and dense subset of , Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point).
If both one-sided limits of a function at exist and differ, the two-sided limit does not exist (If 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 at , as limits of the restrictions of to and , The - limit of at a limit point of ).
Absolute value: for and for ; for and for (Absolute value in an ordered field, Basic properties of the absolute value, Ordered field, Complete ordered field (least-upper-bound property)).
Counterexample
is bounded, with , and continuous at every point of other than : near a point it is locally constant. So is integrable on , and likewise on and on , by [L1].
Assume [A1]. Then everywhere on .
On the function agrees with the constant except at the single point , so by [L2]; on it agrees with the constant except at , so .
On the function is continuous, by [L5], and differentiable at every interior point with ; so is constant on by [L4], say there.
On the function is continuous and differentiable at every with ; so on .
By [L3], .
By [L3] again, equals for and equals for , by [L2] applied on the relevant piece; in both cases by [L7].
Evaluating both formulas at gives ; write for the common value, so for every by [L7].
The difference quotient of at is , which equals for and for by [L7]; so its right-hand limit at is and its left-hand limit is .
By [L6] the two-sided limit of that quotient at does not exist, so is not differentiable at ; this contradicts [A1].
Hence no such exists: is integrable on by step 1.1 and has no primitive there, so the claim is false.
Remarks
-
Darboux's theorem is not used. The slick argument — a derivative has the intermediate value property, and 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 whose derivative vanishes at every interior point of is constant on ; 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. is differentiable with at every point of except , which is exactly what The first fundamental theorem: if is integrable on and continuous at , then ; in particular a continuous has as a primitive promises, since is continuous exactly off . What fails is the existence of any function differentiable at too with derivative there, and step 4.1 shows the obstruction is the jump of at , not a defect of .
-
The value 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 is not differentiable at at all and therefore cannot have any prescribed derivative there.
Depends on
The first fundamental theorem: if is integrable on and continuous at , then ; in particular a continuous has as a primitive
A bounded function on that is continuous except at finitely many points is Riemann integrable
For : is integrable on if and only if it is integrable on and on , and then ; with the oriented form for arbitrary
Changing an integrable function at finitely many points changes neither its integrability nor its integral
If on then for every partition ; in particular every constant function is integrable, with
A function continuous on an interval whose derivative vanishes at every interior point of is constant on ; consequently two such functions with the same derivative differ by a constant
A function differentiable at is continuous at
If 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 at , as limits of the restrictions of to and
The derivative of at a point that is a limit point of , and differentiability on a set
The - limit of at a limit point of
The integral function of an integrable
Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point
Discontinuity at a domain point: removable, jump and essential cases, and the first- and second-kind grouping
The integral with oriented limits: and
The lower and upper Darboux integrals of a bounded on as and , Darboux integrability as their equality, and the notation
Absolute value in an ordered field
Basic properties of the absolute value
Intervals of : the nine order-convex forms, nondegeneracy, and length
Lower bound, bounded below, bounded set
Limit point, isolated point, adherent point, derived set, and dense subset of
Ordered field
Complete ordered field (least-upper-bound property)