CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

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) = x$ on $[0, 1)$ with $f (1) = 0$ is differentiable at every point of $(0, 1)$ with $f^{'} \equiv 1$ , yet no $c$ satisfies $f (1) - f (0) = f^{'} (c)$ , so continuity on the closed interval cannot be dropped from the mean value theorem

Statement refuted

Refuted claim: let $a, b \in R$ with $a < b$ and let $f : [a, b] \to R$ be differentiable at every point of $(a, b)$ as a function on $[a, b]$ (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). Then there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ .

That is The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ with the hypothesis of continuity on $[a, b]$ deleted, and it is false; the false statement itself is recorded as FALSE: differentiability at every point of $(a, b)$ alone yields a $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ . This item works the witness out: it locates the failure at a single point, measures it, and shows that repairing that one value restores the conclusion.

Facts & Assumptions

Given: The function $f : [0, 1] \to R$ with $f (x) : = x$ for $x \in [0, 1)$ and $f (1) : = 0$ , and the identity $h : [0, 1] \to R$ , $h (x) : = x$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L1]

The refutation of FALSE: differentiability at every point of $(a, b)$ alone yields a $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ establishes, for this $f$ : that $f$ is differentiable at every $c \in (0, 1)$ with $f^{'} (c) = 1$ ; that $f (0) = f (1) = 0$ , so $f (1) - f (0) = 0$ ; and that no $c \in (0, 1)$ satisfies $f (1) - f (0) = f^{'} (c) (1 - 0)$ .

[L2]

One-sided limits (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)$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length): the left limit of $f$ at $p$ is the limit at $p$ of $f$ restricted to $[0, 1] \cap (- \infty, p)$ , defined when $p$ is a limit point of that set; the right limit is the same with $[0, 1] \cap (p, \infty)$ .

[L3]

The limit condition (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ): $\lim_{x \to p} u (x) = L$ means that for every real $ε > 0$ there is a real $δ > 0$ such that every $x$ in the domain of $u$ with $0 < ∣ x - p ∣ < δ$ satisfies $∣ u (x) - L ∣ < ε$ . The clause $0 < ∣ x - p ∣$ removes $x = p$ from the quantifier (Basic properties of the absolute value, The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ).

[L4]

Continuity at a limit point (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, clause 1): for $p \in [0, 1]$ a limit point of $[0, 1]$ , the function $f$ is continuous at $p$ if and only if $\lim_{x \to p} f (x)$ exists and equals $f (p)$ .

[L5]

Mean value theorem (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ) and Rolle's theorem (Rolle's theorem: if $a < b$ , $f$ is continuous on $[a, b]$ , differentiable at every point of $(a, b)$ , and $f (a) = f (b)$ , then $f^{'} (c) = 0$ for some $c \in (a, b)$ ), both of which additionally require continuity on the closed interval.

[L6]

The identity on $[0, 1]$ is continuous on $[0, 1]$ and differentiable at every point of $[0, 1]$ with derivative $1$ , its difference quotient at any $c$ being the constant $1$ (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, The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ , 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).

[L7]

$0 \neq 1$ , since $0 < 1$ (The multiplicative identity is positive).

Counterexample

technique · direct

1.1

By [L1] the function $f$ is differentiable at every $c \in (0, 1)$ with $f^{'} (c) = 1$ , satisfies $f (0) = f (1) = 0$ , and admits no $c \in (0, 1)$ with $f (1) - f (0) = f^{'} (c) (1 - 0)$ . So the refuted claim fails at $a : = 0$ , $b : = 1$ .

1.2

The point $1$ is a limit point of $[0, 1]$ and of $[0, 1] \cap (- \infty, 1) = [0, 1)$ : for every real $ε > 0$ the point $y : = \max {1 - ε / 2, 1 / 2}$ satisfies $1 / 2 \leq y < 1$ , hence $y \in [0, 1)$ , and $0 < ∣ y - 1 ∣ \leq ε / 2 < ε$ .

L2L3

2.1

$\lim_{x \to 1} f (x) = 1$ , the limit taken over the domain $[0, 1]$ . Given a real $ε > 0$ , take $δ : = ε$ ; every $x \in [0, 1]$ with $0 < ∣ x - 1 ∣ < δ$ has $x \neq 1$ by [L3], hence $x \in [0, 1)$ and $f (x) = x$ , so $∣ f (x) - 1 ∣ = ∣ x - 1 ∣ < ε$ . Since the same quantifier ranges over the same points when the domain is cut down to $[0, 1)$ , this also says $\lim_{x \to 1^{-}} f (x) = 1$ by [L2]. The right limit at $1$ is not defined, since $[0, 1] \cap (1, \infty)$ is empty and $1$ is therefore not a limit point of it.

step 1.2L2L3

3.1

$f$ is not continuous at $1$ . By step 1.2 the point $1$ is a limit point of $[0, 1]$ , so [L4] makes continuity there equivalent to $\lim_{x \to 1} f (x) = f (1)$ ; by step 2.1 the left side is $1$ and by [L1] the right side is $0$ , and $0 \neq 1$ by [L7]. So exactly one hypothesis of [L5] fails, at exactly one point, and it is the deleted one.

step 2.1L1L4L5L7

4.1

The repair. The identity $h$ agrees with $f$ at every point of $[0, 1]$ except $1$ , where $h (1) = 1$ and $f (1) = 0$ . By [L6] the function $h$ is continuous on $[0, 1]$ and differentiable at every point of $(0, 1)$ with $h^{'} (c) = 1$ , so [L5] applies to $h$ ; and indeed $h (1) - h (0) = 1 = 1 \cdot (1 - 0) = h^{'} (c) (1 - 0)$ for every $c \in (0, 1)$ . So moving the single value $f (1)$ back to $1$ turns a function with no admissible $c$ into one for which every $c$ is admissible.

step 1.1step 3.1L5L6

5.1

The same witness refutes the corresponding weakening of Rolle's theorem: $f (0) = f (1) = 0$ by step 1.1, and yet $f^{'} (c) = 1 \neq 0$ at every $c \in (0, 1)$ by step 1.1 and [L7]. So neither theorem in [L5] survives the deletion of continuity on the closed interval.

step 1.1step 4.1L5L7∎

Remarks

The discontinuity is of the mildest possible kind. Both of the quantities that exist at $1$ , the left limit and the value, exist and are finite; they simply differ. In the vocabulary of the page on monotone functions and discontinuities this is a removable discontinuity, and step 4.1 removes it. Nothing pathological is needed to break the mean value theorem.
Why the derivative sees nothing. The difference quotient of $f$ at an interior $c$ is evaluated only at points within $\min {c, 1 - c}$ of $c$ , and every such point lies in $[0, 1)$ , where $f$ is the identity. So $f^{'}$ carries no information at all about $f (1)$ , while the conclusion of the mean value theorem is an equation containing $f (1)$ . Continuity on the closed interval is precisely the bridge between the two.
Reflecting the witness covers the other endpoint. The function $x \mapsto - f (1 - x)$ is differentiable at every point of $(0, 1)$ with the same constant derivative and fails continuity at $0$ instead of at $1$ , so nothing is special about which endpoint is broken.

Depends on

Used by

Nothing in the library uses this result yet.

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

Mean value theorem (Wikipedia) (standard reference, not scraped)
Rolle's theorem (Wikipedia) (standard reference, not scraped)
Classification of discontinuities (Wikipedia) (standard reference, not scraped)
J. Lebl, Basic Analysis I, Mean Value Theorem (standard reference, not scraped)

f(x)=xf(x)=x on [0,1)[0,1) with f(1)=0f(1)=0 is differentiable at every point of (0,1)(0,1) with f′≡1f′≡1, yet no cc satisfies f(1)−f(0)=f′(c)f(1)−f(0)=f′(c), so continuity on the closed interval cannot be dropped from the mean value theorem