CounterexampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-10 (gpt-5.6-terra-codex-subscription)

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.

A curve for which the mean value inequality is an equality, showing the constant cannot be improved

Statement refuted

Refuted claim: the inequality of The mean value inequality: if $f : [a,b] \to \mathbb{R}^m$ is continuous and differentiable on $(a,b)$ with $\lVert f'\rVert_2 \le M$ , then $\lVert f(b)-f(a)\rVert_2 \le M(b-a)$ can be improved: there is a real $c < 1$ such that for every $m \ge 1$ , every $a<b$ and every $f : [a,b] \to \mathbb{R}^{m}$ continuous on $[a,b]$ and differentiable on $(a,b)$ with $\lVert f'\rVert_2 \le M$ there,

$\lVert f(b)-f(a)\rVert_2 \;\le\; c\,M\,(b-a).$

The witness. Take $m = 2$ , $[a,b] = [0,1]$ and $f : [0,1] \to \mathbb{R}^{2}$ with $f_0(t) = t$ and $f_1(t) = 0$ . Then $\lVert f'(t)\rVert_2 = 1$ for every $t \in (0,1)$ , so $M = 1$ is admissible, and

$\lVert f(1)-f(0)\rVert_2 \;=\; 1 \;=\; M\,(1-0).$

The inequality of The mean value inequality: if $f : [a,b] \to \mathbb{R}^m$ is continuous and differentiable on $(a,b)$ with $\lVert f'\rVert_2 \le M$ , then $\lVert f(b)-f(a)\rVert_2 \le M(b-a)$ is therefore an equality on this curve, and no constant smaller than $1$ can stand in front of $M(b-a)$ .

Facts & Assumptions

Given: The function $f : [0,1] \to \mathbb{R}^{2}$ with $f_0(t) = t$ and $f_1(t) = 0$ .

[A1]

The refuted claim: there is a real $c<1$ with $\lVert f(b)-f(a)\rVert_2 \le c\,M(b-a)$ in the situation of The mean value inequality: if $f : [a,b] \to \mathbb{R}^m$ is continuous and differentiable on $(a,b)$ with $\lVert f'\rVert_2 \le M$ , then $\lVert f(b)-f(a)\rVert_2 \le M(b-a)$ .

[L1]

Derivatives of powers: $t \mapsto t$ is differentiable at every real with derivative $1$ , and a constant function has derivative $0$ (For a natural $n \ge 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $\iota(n)\,x^{\,n-1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \ge 1$ the function $x \mapsto x^{-n}$ is differentiable at every $x \ne 0$ with derivative $-\iota(n)\,x^{-n-1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term claims 1 and 2, The derivative $f'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c}$ of $f : A \to \mathbb{R}$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, Integer powers $a^m$ , The canonical natural $\iota(n) = n \cdot 1_F$ of a field).

[L2]

A vector-valued function is differentiable at a point exactly when each component is, with $f'(t)_i = f_i'(t)$ , and is continuous when each component is (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions, Vector-valued functions $f : A \to \mathbb{R}^m$ , their limits and continuity, with the dictionary to the metric notions, A function differentiable at $c$ is continuous at $c$ , Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function).

[L3]

The Euclidean norm on $\mathbb{R}^{2}$ : $\lVert y\rVert_2 = \sqrt{y_0^{2}+y_1^{2}}$ , and $\sqrt{1} = 1$ (The $p$ -norms $\lVert x\rVert_p$ for rational $p \ge 1$ , and $\lVert x\rVert_\infty$ , The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$ , A norm on a real vector space, the induced metric, and the dictionary with the metric axioms, Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$ ; the positives are $\{x^2 : x \neq 0\}$ ).

[L4]

The mean value inequality (The mean value inequality: if $f : [a,b] \to \mathbb{R}^m$ is continuous and differentiable on $(a,b)$ with $\lVert f'\rVert_2 \le M$ , then $\lVert f(b)-f(a)\rVert_2 \le M(b-a)$ , Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length).

[L5]

$1 > 0$ and $\iota$ is positive on the naturals $\ge 1$ (Canonical naturals are positive and strictly increasing, The canonical natural $\iota(n) = n \cdot 1_F$ of a field).

Counterexample

technique · direct

1.1

Each component of $f$ is differentiable at every real, with $f_0'(t) = 1$ and $f_1'(t) = 0$ ; so $f$ is differentiable at every $t \in [0,1]$ with $f'(t) = (1,0)$ , and $f$ is continuous on $[0,1]$ .

L1L2

1.2

$f(1) = (1,0)$ and $f(0) = (0,0)$ , so $f(1)-f(0) = (1,0)$ and $\lVert f(1)-f(0)\rVert_2 = 1$ .

2.1

$\lVert f'(t)\rVert_2 = \sqrt{1^{2}+0^{2}} = 1$ for every $t$ , so $M := 1$ satisfies the hypothesis $\lVert f'\rVert_2 \le M$ on $(0,1)$ , and $M \ge 0$ .

step 1.1L3

3.1

The conclusion of The mean value inequality: if $f : [a,b] \to \mathbb{R}^m$ is continuous and differentiable on $(a,b)$ with $\lVert f'\rVert_2 \le M$ , then $\lVert f(b)-f(a)\rVert_2 \le M(b-a)$ on this curve reads $1 \le M(1-0) = 1$ : the inequality holds and is an equality.

step 2.1step 1.2L4

4.1

Suppose [A1] held with some real $c<1$ . Applied to this curve it would give $1 \le c\cdot 1\cdot 1 = c < 1$ , which is impossible. So no constant smaller than $1$ works, and [A1] is false.

step 1.2step 3.1A1L5∎

Remarks

The two witnesses on this page say opposite-looking things and are consistent. $f(t) = (t^{2}, t^{3})$ on $[0,1]$ : no $\xi$ satisfies $f(1)-f(0) = f'(\xi)$ shows that the equality form of the mean value theorem fails for $m \ge 2$ : there need be no $\xi$ with $f(b)-f(a) = f'(\xi)(b-a)$ . The present item shows that the inequality of The mean value inequality: if $f : [a,b] \to \mathbb{R}^m$ is continuous and differentiable on $(a,b)$ with $\lVert f'\rVert_2 \le M$ , then $\lVert f(b)-f(a)\rVert_2 \le M(b-a)$ is nevertheless sharp. Together they say that the correct vector-valued statement is an inequality, and that it is the best inequality of its shape.
Why the equality is attained here and not there. On the curve above the derivative is constant, so it points in one direction and the displacement accumulates with no cancellation. On $t \mapsto (t^{2},t^{3})$ the direction of $f'$ turns as $t$ increases, and the displacement is strictly shorter than the length the bound allows: there $\lVert f(1)-f(0)\rVert_2 = \sqrt{2}$ while the bound is $\sqrt{\iota(13)}$ .
The curve is as simple as it can be. Its image is a segment of the first coordinate axis, and the second component is present only so that the codomain is $\mathbb{R}^{2}$ rather than $\mathbb{R}^{1}$ ; the same computation in $\mathbb{R}^{m}$ for any $m \ge 1$ gives the same equality.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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

Mean value theorem (Wikipedia) (standard reference, not scraped)
Vector-valued function (Wikipedia) (standard reference, not scraped)
J. Lebl, Basic Analysis I, Section 8.4 (standard reference, not scraped)