CounterexampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-09 (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.

$x \mapsto \sqrt{x}$ on $(0,1]$ is differentiable with unbounded derivative and is not Lipschitz there, so the boundedness hypothesis in the Lipschitz corollary cannot be dropped

Statement refuted

Refuted claim: let $I \subseteq \mathbb{R}$ be order-convex (Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length) and let $h : I \to \mathbb{R}$ be continuous on $I$ and differentiable at every interior point of $I$ (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). Then $h$ is Lipschitz on $I$ , that is, there is a real $L \ge 0$ with $|h(x)-h(y)| \le L|x-y|$ for all $x, y \in I$ (Lipschitz map, $\alpha$ -Hölder map for rational $0 < \alpha \le 1$ , and contraction, clause 3 of Dictionary: for $A \subseteq \mathbb{R}$ with the metric $d(x,y) = |x-y|$ , continuity and uniform continuity of $f : A \to \mathbb{R}$ agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of $\mathbb{R}$ is compact in the open-cover sense of $\mathbb{R}$ exactly when it is a compact metric subspace).

That is If $f$ is continuous on an interval $I$ and $|f'| \le M$ at every interior point, then $|f(x) - f(y)| \le M|x-y|$ for all $x,y \in I$ , so $f$ is Lipschitz with constant $M$ and uniformly continuous on $I$ with the hypothesis $|h'| \le M$ deleted. It is false, and the witness is the square root on $(0,1]$ : an interval on which the derivative exists at every interior point and is bounded above by no real.

Facts & Assumptions

Given: The set $I := (0,1]$ , order-convex with at least two elements (Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length), and the function $s : I \to \mathbb{R}$ , $s(b) := b^{1/2}$ , the nonnegative square root (Existence and uniqueness of $n$ -th roots: a unique $a^{1/n} \ge 0$ with $(a^{1/n})^n = a$ , Rational powers $a^r$ of a positive base); numerals denote canonical naturals (The canonical natural $\iota(n) = n \cdot 1_F$ of a field).

[L1]

Derivative of the square root (For a natural $n \ge 1$ , the derivative of $x \mapsto x^{1/n}$ on $(0,\infty)$ is $\frac{1}{\iota(n)}x^{1/n - 1}$ , obtained from the inverse rule applied to $x \mapsto x^{n}$ ; in particular $(\sqrt{x})' = 1/(\iota(2)\sqrt{x})$ , at $n = 2$ , with the restriction clause of 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 and $I \subseteq (0,\infty)$ ): $s$ is differentiable at every $b \in I$ with $s'(b) = \frac{1}{\iota(2)}b^{-1/2}$ , every point of $I$ being a limit point of $I$ (Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$ ).

[L2]

A function differentiable at a point is continuous there (A function differentiable at $c$ is continuous at $c$ ).

[L3]

Uniqueness of the nonnegative square root (Existence and uniqueness of $n$ -th roots: a unique $a^{1/n} \ge 0$ with $(a^{1/n})^n = a$ ): for $a \ge 0$ there is exactly one $t \ge 0$ with $t^{2} = a$ , and it is $a^{1/2}$ (Rational powers $a^r$ of a positive base, Integer powers $a^m$ ).

[L4]

Rational powers (Laws of rational exponents, Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ ): $a^{r} > 0$ for $a > 0$ ; $a^{-r} = 1/a^{r}$ ; $(a^{r})^{s} = a^{rs}$ ; and for rational $r > 0$ , $0 < a < b$ implies $a^{r} < b^{r}$ (claim 2 of the monotonicity lemma).

[L5]

Archimedean property in reciprocal form (For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$ , Every complete ordered field is Archimedean): for every real $\varepsilon > 0$ there is a natural $m \ge 1$ with $1/\iota(m) < \varepsilon$ .

[L6]

Order and numeral arithmetic (Inverses of positives are positive, and reciprocation reverses order, Sign rules for products and monotonicity of multiplication, Multiplying inequalities of positives, Canonical naturals are positive and strictly increasing, Monotonicity of $x \mapsto x^n$ and of $n \mapsto a^n$ , Basic properties of the absolute value, The canonical natural $\iota(n) = n \cdot 1_F$ of a field): $\iota(m) > 0$ for $m \ge 1$ ; $0 < a < b$ gives $0 < 1/b < 1/a$ (Inverses of positives are positive, and reciprocation reverses order); a product of positives is positive and multiplying a STRICT inequality by a positive real preserves it (Sign rules for products and monotonicity of multiplication); the NONSTRICT form, $0 \le x \le y$ and $0 \le u \le v$ imply $xu \le yv$ , is not stated by Sign rules for products and monotonicity of multiplication, whose multiplicative claims are strict, but by Multiplying inequalities of positives, and it is what licenses both multiplying a $\le$ by a positive real and dividing a $\le$ by one, the divisor entering as its positive inverse; $0 \le a \le b$ gives $a^{2} \le b^{2}$ (Monotonicity of $x \mapsto x^n$ and of $n \mapsto a^n$ , claim 2); $|u| = u$ for $u \ge 0$ (Basic properties of the absolute value); and $\iota(mn) = \iota(m)\iota(n)$ and $\iota(m+n) = \iota(m)+\iota(n)$ for naturals $m, n \ge 1$ , so $\iota(2)^{2} = \iota(4)$ , $\iota(2) - 1 = 1$ and $\iota(4) - 1 = \iota(3)$ .

[L7]

Interiority and boundedness (Interior, closure, boundary and exterior of a subset of $\mathbb{R}$ , The $\varepsilon$ -neighbourhood and the punctured $\varepsilon$ -neighbourhood of a point of $\mathbb{R}$ , Lower bound, bounded below, bounded set): $p$ is interior to $S$ exactly when $N_{\varepsilon}(p) \subseteq S$ for some real $\varepsilon > 0$ ; and a set of reals is bounded above when some real exceeds or equals all of its elements.

[L8]

The corollary under test (If $f$ is continuous on an interval $I$ and $|f'| \le M$ at every interior point, then $|f(x) - f(y)| \le M|x-y|$ for all $x,y \in I$ , so $f$ is Lipschitz with constant $M$ and uniformly continuous on $I$ ) additionally requires a real $M \ge 0$ with $|h'| \le M$ at every interior point.

Counterexample

technique · direct

1.1

By [L1] the function $s$ is differentiable at every $b \in I$ with $s'(b) = \frac{1}{\iota(2)}b^{-1/2} > 0$ , using [L4] and [L6]; and by [L2] it is continuous at every point of $I$ , hence continuous on $I$ .

L1L2L4L6

1.2

The interior points of $I = (0,1]$ are exactly the reals $b$ with $0 < b < 1$ : for such a $b$ the neighbourhood $N_{\rho}(b)$ with $\rho := \min\{b,\ 1-b\} > 0$ lies in $(0,1) \subseteq I$ ; the point $1$ is not interior, since $1 + \varepsilon/2 \in N_{\varepsilon}(1)$ and $1 + \varepsilon/2 \notin I$ for every real $\varepsilon > 0$ ; and every interior point lies in $I$ .

2.1

The derivative is bounded above by no real. Let $K$ be a real. If $K \le 0$ , any $b$ with $0 < b < 1$ has $s'(b) > 0 \ge K$ by step 1.1. If $K > 0$ , put $\beta := \bigl(1/(\iota(2)K)\bigr)^{2}$ , a positive real, and use [L5] to fix a natural $m \ge 1$ with $1/\iota(m) < \min\{\beta,\ 1\}$ ; put $b := 1/\iota(m)$ , so $0 < b < 1$ and $b < \beta$ . By [L4], $b^{1/2} < \beta^{1/2} = \bigl(1/(\iota(2)K)\bigr)^{2 \cdot (1/2)} = 1/(\iota(2)K)$ , so $b^{-1/2} = 1/b^{1/2} > \iota(2)K$ by [L6], and hence $s'(b) = \frac{1}{\iota(2)}b^{-1/2} > K$ . So for every real $K$ there is an interior point $b$ of $I$ with $s'(b) > K$ , and the set of values of $s'$ on the interior of $I$ is bounded above by no real.

step 1.1step 1.2L4L5L6L7

2.2

$s$ is not Lipschitz on $I$ . Suppose some real $L \ge 0$ satisfied $|s(x)-s(y)| \le L|x-y|$ for all $x, y \in I$ . Let $t$ be a real with $0 < t \le 1/\iota(2)$ , and put $x := t^{2}$ and $y := \iota(4)t^{2}$ . Then $0 < x \le y = \iota(4)t^{2} \le \iota(4)/\iota(4) = 1$ , so $x, y \in I$ ; and $s(x) = t$ and $s(y) = \iota(2)t$ by [L3], since $t \ge 0$ with $t^{2} = x$ and $\iota(2)t \ge 0$ with $(\iota(2)t)^{2} = \iota(4)t^{2} = y$ . Hence $|s(y)-s(x)| = \iota(2)t - t = t$ and $|y - x| = \iota(3)t^{2}$ by [L6], and the supposition gives $t \le L\,\iota(3)t^{2}$ ; dividing by $t > 0$ gives $1 \le \iota(3)Lt$ for every such $t$ . Taking $t := 1/\iota(2)$ shows $\iota(3)L/\iota(2) \ge 1$ , so $L > 0$ . Now use [L5] to fix a natural $m \ge 1$ with $1/\iota(m) < 1/(\iota(3)L)$ and put $t := \min\{1/\iota(m),\ 1/\iota(2)\}$ , a real with $0 < t \le 1/\iota(2)$ ; then $\iota(3)Lt \le \iota(3)L/\iota(m) < 1$ , contradicting $1 \le \iota(3)Lt$ . So no such $L$ exists.

step 1.1L3L4L5L6

3.1

The refuted claim therefore fails at $I := (0,1]$ and $h := s$ : by step 1.1 the function $s$ is continuous on the order-convex set $I$ and differentiable at every point of $I$ , in particular at every interior point of $I$ by step 1.2, and yet by step 2.2 it is not Lipschitz on $I$ . Nothing in [L8] is contradicted: by step 2.1 no real $M$ bounds $|s'|$ on the interior of $I$ , so the hypothesis deleted from that corollary is exactly the one that fails.

step 1.1step 1.2step 2.1step 2.2L8∎

Remarks

The two failures are separate statements, and both are proved. That the derivative is unbounded (step 2.1) does not by itself refute the claim, since the claim is about a Lipschitz bound and not about $s'$ ; and the Lipschitz bound is refuted directly, by a pair of points whose square roots differ by $t$ while the points themselves differ by $\iota(3)t^{2}$ . Only step 2.1 is needed to say which hypothesis of If $f$ is continuous on an interval $I$ and $|f'| \le M$ at every interior point, then $|f(x) - f(y)| \le M|x-y|$ for all $x,y \in I$ , so $f$ is Lipschitz with constant $M$ and uniformly continuous on $I$ is the one that fails.
Contrast with the same function on $[1,\infty)$ . There the derivative is bounded by $1/\iota(2)$ and the corollary applies, which is The mean value theorem gives $|\sqrt{x} - \sqrt{y}| \le \tfrac{1}{\iota(2)} |x - y|$ for $x, y \ge 1$ , so the square root is Lipschitz with constant $1/2$ on $[1,\infty)$ on this page. The function is the same; the interval is what decides. That is the sense in which the Lipschitz property is a property of the pair (function, domain), exactly as Uniform continuity of $f : A \to \mathbb{R}$ : one $\delta$ serving every pair of points of $A$ records for uniform continuity.
What is not claimed. This item asserts the failure of the Lipschitz condition on $(0,1]$ and nothing more. In particular nothing above says whether $s$ is uniformly continuous on $(0,1]$ , nor whether it satisfies a Hölder condition of some exponent below $1$ there; those are separate questions, and no item on this page is entitled to be cited for either.

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: 148 results over 32 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

Lipschitz continuity (Wikipedia) (standard reference, not scraped)
Square root (Wikipedia) (standard reference, not scraped)
Archimedean property (Wikipedia) (standard reference, not scraped)
J. Hunter, An Introduction to Real Analysis (standard reference, not scraped)
MIT 18.785 Number Theory I, Lecture 19 (standard reference, not scraped)

x↦xx \mapsto \sqrt{x}x↦x​ on (0,1](0,1](0,1] is differentiable with unbounded derivative and is not Lipschitz there, so the boundedness hypothesis in the Lipschitz corollary cannot be dropped