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.

✓ 6 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 6 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Total Derivative: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

The polynomial map $(x, y) \mapsto (1 + x + 2 y + x^{2}, 2 x + 3 y + x y)$ and its Jacobian

Example

Let $F (x, y) = (1 + x + 2 y + x^{2}, 2 x + 3 y + x y)$ . Then $F$ is totally differentiable everywhere and

$D F (x, y) = J F (x, y) = (\begin{array}{cc} 1 + 2 x & 2 \\ 2 + y & 3 + x \end{array}) .$

Facts & Assumptions

Given: The polynomial map $F : R^{2} \to R^{2}$ .

[L1]

The function $x \mapsto x^{n}$ is differentiable everywhere with derivative $n x^{n - 1}$ for positive natural $n$ (For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term).

[L2]

Continuous partial derivatives imply total differentiability with Jacobian derivative (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).

Verification

technique · direct

1.1

The four partial derivatives are $1 + 2 x$ , $2$ , $2 + y$ , and $3 + x$ , by [L1] and derivative algebra.

L1L2

2.1

These polynomial partial derivatives are continuous everywhere, so [L2] gives total differentiability and identifies the derivative with the displayed Jacobian.

step 1.1L2algebra

3.1

Directly, the increment remainder is $(h_{1}^{2}, h_{1} h_{2})$ , whose norm divided by $∥ (h_{1}, h_{2}) ∥_{2}$ tends to zero, agreeing with step 2.1.

step 1.1step 2.1∎

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

$x y / (x^{2} + y^{2})$ has both partial derivatives at the origin but is discontinuous there

Statement refuted

If both partial derivatives of a real function exist at a point, then the function is continuous there.

Facts & Assumptions

Given: The function $f (0, 0) = 0$ and $f (x, y) = x y / (x^{2} + y^{2})$ when $(x, y) \neq (0, 0)$ .

[L1]

Partial derivatives are directional derivatives in the standard basis directions (Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ).

[L2]

A map is continuous at $a$ if its values tend to $f (a)$ as the input tends to $a$ (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form).

Counterexample

technique · direct

1.1

Both axis restrictions of $f$ are identically zero, so [L1] gives $\partial_{x} f (0, 0) = \partial_{y} f (0, 0) = 0$ .

L1L2

2.1

On the punctured diagonal $(t, t)$ , $f (t, t) = 1 / 2$ .

step 1.1L2algebra

3.1

As $(t, t) \to (0, 0)$ but the values in step 2.1 do not tend to $f (0, 0) = 0$ , [L2] shows that $f$ is discontinuous at the origin.

step 1.1step 2.1∎

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

$x^{2} y / (x^{4} + y^{2})$ tends to zero on every line through the origin but not along $y = x^{2}$

Statement refuted

If a function tends to its proposed value along every straight line through a point, then it is continuous at that point.

Facts & Assumptions

Given: $f (0, 0) = 0$ and $f (x, y) = x^{2} y / (x^{4} + y^{2})$ away from the origin.

[L1]

A vector-valued map is continuous at $a$ when its limit at $a$ equals its value there (Vector-valued functions $f : A \to R^{m}$ , their limits and continuity, with the dictionary to the metric notions).

Counterexample

technique · direct

1.1

On a line $(x, y) = (t a, t b)$ with $b \neq 0$ , $f (t a, t b) = t a^{2} b / (t^{2} a^{4} + b^{2}) \to 0$ ; for $b = 0$ the restriction is identically zero.

2.1

Along the parabola $(x, y) = (t, t^{2})$ with $t \neq 0$ , $f (t, t^{2}) = 1 / 2$ .

step 1.1algebra

3.1

The nonlinear path tends to the origin but its values do not tend to $0$ , so [L1] shows that $f$ is not continuous there despite all straight-line tests.

step 1.1step 2.1∎

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

$x^{2} y / (x^{2} + y^{2})$ has every directional derivative at the origin but is not totally differentiable there

Statement refuted

If every directional derivative of a real function exists at a point, then the function is totally differentiable there.

Facts & Assumptions

Given: $f (0, 0) = 0$ and $f (x, y) = x^{2} y / (x^{2} + y^{2})$ away from the origin.

[L1]

The directional derivative is the derivative of $t \mapsto f (a + t v)$ at zero (Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ).

[L2]

A total derivative computes every directional derivative, so $v \mapsto D_{v} f (a)$ would be the linear map $D f (a)$ applied to $v$ (A total derivative computes every directional derivative, and its matrix is the Jacobian).

Counterexample

technique · direct

1.1

For $v = (a, b) \neq 0$ , $f (t a, t b) = t a^{2} b / (a^{2} + b^{2})$ , so [L1] gives $D_{v} f (0, 0) = a^{2} b / (a^{2} + b^{2})$ ; for $v = 0$ it is $0$ .

L1L2

2.1

This direction map has value $0$ at $(1, 0)$ and $(0, 1)$ but value $1 / 2$ at their sum $(1, 1)$ , so it is not additive.

step 1.1L2algebra

3.1

By [L2], total differentiability would make the directional-derivative map linear, contradicting step 2.1. Thus $f$ is not totally differentiable at the origin.

step 1.1step 2.1∎

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

The map $y (x^{2} + y^{2}) / x$ off the line $x = 0$ , extended by zero on that line, has every directional derivative zero at the origin but is discontinuous there

Statement refuted

If every directional derivative at a point is zero, then the function is continuous there.

Facts & Assumptions

Given: $f (x, y) = y (x^{2} + y^{2}) / x$ for $x \neq 0$ , and $f (0, y) = 0$ .

[L1]

The directional derivative is the derivative of $t \mapsto f (a + t v)$ at zero (Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ).

[L2]

Total differentiability gives a local $O (∥ h ∥_{2})$ increment bound and therefore continuity (Total differentiability gives a local $O (∥ h ∥_{2})$ increment bound and therefore continuity).

Counterexample

technique · direct

1.1

Along $(t a, t b)$ , the restriction is $t^{2} b (a^{2} + b^{2}) / a$ when $a \neq 0$ and is $0$ when $a = 0$ ; [L1] therefore gives zero directional derivative in every direction.

L1L2

2.1

Along the curve $(x, y) = (t^{3}, t)$ with $t \neq 0$ , $f (t^{3}, t) = 1 + t^{4} \to 1$ .

step 1.1L2algebra

3.1

Thus $f$ is discontinuous at the origin, and by [L2] it cannot be totally differentiable there either.

step 1.1step 2.1∎

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

A locally constant step map on the disconnected open set $R ∖ {0}$ has zero total derivative but is not globally Lipschitz

Statement refuted

A uniform total-derivative bound on every open domain implies a global Lipschitz bound on that domain.

Facts & Assumptions

Given: $U = R ∖ {0}$ and $f : U \to R$ defined by $f (x) = 0$ for $x < 0$ and $f (x) = 1$ for $x > 0$ .

[L1]

In the total-derivative definition, the normalized remainder tends to zero as $h$ tends to zero (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder).

[L2]

A map is Lipschitz with constant $L$ when $∣ f (x) - f (y) ∣ \leq L ∣ x - y ∣$ for every pair of points in its domain (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction).

Counterexample

technique · direct

1.1

Each $x \in U$ has a small interval contained in its own component of $U$ , on which $f$ is constant; hence $D f (x) = 0$ by [L1].

L1L2

2.1

For any $L \geq 0$ , take $t = 1 / (2 (L + 1))$ . The points $- t, t \in U$ satisfy $∣ f (t) - f (- t) ∣ = 1 > 2 L t = L ∣ t - (- t) ∣$ , so [L2] fails for that $L$ .

step 1.1L2algebra

3.1

The segment from $- t$ to $t$ contains $0 \notin U$ , so $U$ is not convex; this is exactly the omitted hypothesis of the mean-value inequality.

step 1.1step 2.1∎

The Total Derivative: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

The polynomial map (x,y)↦(1+x+2y+x2, 2x+3y+xy)(x,y)↦(1+x+2y+x2,2x+3y+xy) and its Jacobian

Example

Facts & Assumptions

Verification

xy/(x2+y2)xy/(x2+y2) has both partial derivatives at the origin but is discontinuous there

Statement refuted

Facts & Assumptions

Counterexample

x2y/(x4+y2)x2y/(x4+y2) tends to zero on every line through the origin but not along y=x2y=x2

Statement refuted

Facts & Assumptions

Counterexample

x2y/(x2+y2)x2y/(x2+y2) has every directional derivative at the origin but is not totally differentiable there

Statement refuted

Facts & Assumptions

Counterexample

The map y(x2+y2)/xy(x2+y2)/x off the line x=0x=0, extended by zero on that line, has every directional derivative zero at the origin but is discontinuous there

Statement refuted

Facts & Assumptions

Counterexample

A locally constant step map on the disconnected open set R∖{0}R∖{0} has zero total derivative but is not globally Lipschitz

Statement refuted

Facts & Assumptions

Counterexample

Sources

The polynomial map $(x, y) \mapsto (1 + x + 2 y + x^{2}, 2 x + 3 y + x y)$ and its Jacobian

$x y / (x^{2} + y^{2})$ has both partial derivatives at the origin but is discontinuous there

$x^{2} y / (x^{4} + y^{2})$ tends to zero on every line through the origin but not along $y = x^{2}$

$x^{2} y / (x^{2} + y^{2})$ has every directional derivative at the origin but is not totally differentiable there

The map $y (x^{2} + y^{2}) / x$ off the line $x = 0$ , extended by zero on that line, has every directional derivative zero at the origin but is discontinuous there

A locally constant step map on the disconnected open set $R ∖ {0}$ has zero total derivative but is not globally Lipschitz