CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck 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.

$x \mapsto ∣ x ∣$ is continuous everywhere and not differentiable at $0$ : the difference quotient equals $1$ on the right and $- 1$ on the left, so the two one-sided limits differ

Statement refuted

Refuted claim: if $A \subseteq R$ , if $f : A \to R$ is continuous at a point $c \in 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) and if $c$ is a limit point of $A$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ), then $f$ is differentiable 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).

This is the converse of A function differentiable at $c$ is continuous at $c$ , and it is false. The witness is $f (x) = ∣ x ∣$ on $A = R$ at $c = 0$ : a single corner is enough, and the failure is visible in one line, the difference quotient taking the value $1$ to the right of $0$ and $- 1$ to the left.

Facts & Assumptions

Given: The set $A : = R$ , the function $f : R \to R$ , $f (x) : = ∣ x ∣$ (Basic properties of the absolute value), and the point $c : = 0$ .

[L1]

Continuity of the absolute value (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): the identity is continuous at every point of its domain (claim 5), and $∣ h ∣$ is continuous wherever $h$ is (claim 2); so $f$ is continuous at every point 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).

[L2]

Derivative (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): $0$ is a limit point of $R$ , punctured neighbourhoods being never empty (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ , The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ); the difference quotient of $f$ at $0$ is $q (x) = (∣ x ∣ - ∣ 0 ∣) / (x - 0)$ on $R ∖ {0}$ ; and $f$ is differentiable at $0$ exactly when $\lim_{x \to 0} q (x)$ exists (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).

[L3]

Absolute value (Basic properties of the absolute value): $∣ 0 ∣ = 0$ ; $∣ u ∣ = u$ for $u \geq 0$ ; and $∣ u ∣ = - u$ for $u \leq 0$ .

[L4]

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): for $D \subseteq R$ and $p \in R$ , the right limit of $h : D \to R$ at $p$ is the limit at $p$ of $h$ restricted to $D \cap (p, \infty)$ , defined when $p$ is a limit point of that set, and the left limit is the same with $D \cap (- \infty, p)$ .

[L5]

Two-sided against one-sided (If $c$ is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree): if $p$ is a limit point of both $D \cap (- \infty, p)$ and $D \cap (p, \infty)$ , then for every real $L$ the equality $\lim_{x \to p} h (x) = L$ holds if and only if both one-sided limits at $p$ exist and equal $L$ .

[L6]

At a limit point of its domain a function has at most one limit (At a limit point of the domain a function has at most one limit); and the limit of a constant function $K$ at a limit point of its domain is $K$ , any $δ$ serving (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).

[L7]

$1 \neq - 1$ : $0 < 1$ (The multiplicative identity is positive) gives $- 1 < 0 < 1$ , and trichotomy forbids equality.

Counterexample

technique · direct

1.1

$f$ is continuous at every point of $R$ , in particular at $0$ .

1.2

$f (0) = ∣ 0 ∣ = 0$ , so the difference quotient of $f$ at $0$ is $q (x) = ∣ x ∣ / x$ on $D : = R ∖ {0}$ .

L2L3

1.3

$D \cap (0, \infty) = (0, \infty)$ and $D \cap (- \infty, 0) = (- \infty, 0)$ , and $0$ is a limit point of each: for every real $ε > 0$ the point $ε / 2$ lies in $(0, \infty)$ with $0 < ∣ ε / 2 - 0 ∣ < ε$ , and $- ε / 2$ lies in $(- \infty, 0)$ with $0 < ∣ - ε / 2 - 0 ∣ < ε$ .

L3L4

2.1

For $x > 0$ one has $∣ x ∣ = x$ , so $q (x) = x / x = 1$ ; for $x < 0$ one has $∣ x ∣ = - x$ , so $q (x) = (- x) / x = - 1$ . Thus $q$ restricted to $(0, \infty)$ is the constant $1$ and $q$ restricted to $(- \infty, 0)$ is the constant $- 1$ .

step 1.2L3

3.1

By [L6] and step 1.3 the two restrictions have limits at $0$ , namely $1$ and $- 1$ ; so by [L4] the right limit of $q$ at $0$ is $1$ and the left limit is $- 1$ .

step 1.3step 2.1L4L6

4.1

Suppose $\lim_{x \to 0} q (x) = L$ for some real $L$ . By step 1.3 the point $0$ is a limit point of both one-sided sets, so [L5] forces both one-sided limits to equal $L$ ; with step 3.1 and [L6] that gives $L = 1$ and $L = - 1$ , hence $1 = - 1$ , which [L7] forbids. So $q$ has no limit at $0$ , and by [L2] the function $f$ is not differentiable at $0$ .

step 3.1L2L5L6L7

5.1

The refuted claim therefore fails at $A : = R$ , $f : = ∣ \cdot ∣$ and $c : = 0$ : the point $0$ is a limit point of $R$ , $f$ is continuous at $0$ by step 1.1, and $f$ is not differentiable at $0$ by step 4.1.

step 1.1step 4.1∎

Remarks

The failure is one-sided in a precise sense. Both one-sided limits of the difference quotient exist; they simply disagree. So this is not a function whose difference quotients oscillate or blow up, and the restriction of $f$ to $[0, \infty)$ is differentiable at $0$ with derivative $1$ , as 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 records when it observes that differentiability is a property of the pair (function, domain).
What this says about A function differentiable at $c$ is continuous at $c$ . That implication is strict: continuity is genuinely weaker than differentiability, and this witness shows the gap opens at a single point of an otherwise unremarkable function. Nothing here suggests the gap is small in any other sense; how large the set of non-differentiability of a continuous function can be is not a question this page can pose.
Why the argument needs If $c$ is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree and not merely two computations. Two different one-sided values do not by themselves contradict anything until one knows that a two-sided limit would have to agree with both, and that is exactly what the cited theorem supplies, under the hypothesis that $0$ is approached from both sides inside the domain.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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

Absolute value (Wikipedia) (standard reference, not scraped)
Differentiable function (Wikipedia) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §4.1 (standard reference, not scraped)
T. Gantumur, Differentiation (standard reference, not scraped)

x↦∣x∣x↦∣x∣ is continuous everywhere and not differentiable at 00: the difference quotient equals 11 on the right and −1−1 on the left, so the two one-sided limits differ