Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

xxx \mapsto |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

Statement refuted

Refuted claim: if ARA \subseteq \mathbb{R}, if f:ARf : A \to \mathbb{R} is continuous at a point cAc \in A (Continuity of f:ARf : A \to \mathbb{R} at a point of AA and on AA: the ε\varepsilon-δ\delta condition, its agreement with limxcf(x)=f(c)\lim_{x \to c} f(x) = f(c) at a limit point, and continuity at an isolated point) and if cc is a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}), then ff is differentiable at cc (The derivative f(c)=limxcf(x)f(c)xcf'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c} of f:ARf : A \to \mathbb{R} at a point cAc \in A that is a limit point of AA, and differentiability on a set).

This is the converse of A function differentiable at cc is continuous at cc, and it is false. The witness is f(x)=xf(x) = |x| on A=RA = \mathbb{R} at c=0c = 0: a single corner is enough, and the failure is visible in one line, the difference quotient taking the value 11 to the right of 00 and 1-1 to the left.

Facts & Assumptions

Given: The set A:=RA := \mathbb{R}, the function f:RRf : \mathbb{R} \to \mathbb{R}, f(x):=xf(x) := |x| (Basic properties of the absolute value), and the point c:=0c := 0.

[L3]

Absolute value (Basic properties of the absolute value): 0=0|0| = 0; u=u|u| = u for u0u \ge 0; and u=u|u| = -u for u0u \le 0.

[L4]

One-sided limits (The left and right limits of ff at cc, as limits of the restrictions of ff to A(,c)A \cap (-\infty, c) and A(c,)A \cap (c, \infty), Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length): for DRD \subseteq \mathbb{R} and pRp \in \mathbb{R}, the right limit of h:DRh : D \to \mathbb{R} at pp is the limit at pp of hh restricted to D(p,)D \cap (p, \infty), defined when pp is a limit point of that set, and the left limit is the same with D(,p)D \cap (-\infty, p).

[L5]

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

[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 KK at a limit point of its domain is KK, any δ\delta serving (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA).

[L7]

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

Counterexample

technique · direct
1.1

ff is continuous at every point of R\mathbb{R}, in particular at 00.

L1
1.2

f(0)=0=0f(0) = |0| = 0, so the difference quotient of ff at 00 is q(x)=x/xq(x) = |x|/x on D:=R{0}D := \mathbb{R} \setminus \{0\}.

L2L3
1.3

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

L3L4
2.1

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

step 1.2L3
3.1

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

step 1.3step 2.1L4L6
4.1

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

step 3.1L2L5L6L7
5.1

The refuted claim therefore fails at A:=RA := \mathbb{R}, f:=f := |\cdot| and c:=0c := 0: the point 00 is a limit point of R\mathbb{R}, ff is continuous at 00 by step 1.1, and ff is not differentiable at 00 by step 4.1.

step 1.1step 4.1

Remarks

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: 55 results over 17 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