ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

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.

$\sqrt{\cdot}$ on $[0, \infty)$ is uniformly continuous and exactly $1 / 2$ -Hölder, and is not Lipschitz

Example

Let $X : = [0, \infty) \subseteq R$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length) with the metric $d (x, y) = ∣ x - y ∣$ inherited from $R$ (The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded, Isometry, isometric embedding, and the subspace metric on a subset), and let $g : X \to X$ be $g (x) : = \sqrt{x} = x^{1 / 2}$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Rational powers $a^{r}$ of a positive base). Then:

$∣ \sqrt{x} - \sqrt{y} ∣ \leq ∣ x - y ∣^{1 / 2}$ for all $x, y \geq 0$ , so $g$ is $1 / 2$ -Hölder with constant $1$ (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction).
$g$ is uniformly continuous (Uniform continuity of a map of metric spaces: one $δ$ serving every point).
The constant $1$ cannot be improved: every $1 / 2$ -Hölder constant $C$ for $g$ satisfies $C \geq 1$ .
For every rational $α$ with $1 / 2 < α \leq 1$ , the map $g$ is not $α$ -Hölder. In particular, at $α = 1$ , $g$ is not Lipschitz.

So $1 / 2$ is exactly the Hölder exponent of the square root, and the example separates "Hölder" from "Lipschitz" inside Contraction implies Lipschitz implies uniformly continuous implies continuous; every Hölder map is uniformly continuous, and a Lipschitz map on a bounded space is Hölder for every exponent.

Facts & Assumptions

Given: $X = [0, \infty)$ with the metric inherited from $R$ ; $g (x) = \sqrt{x}$ ; reals $x, y \in X$ ; a rational $α$ with $0 < α \leq 1$ ; a real $C \geq 0$ .

[L1]

Every $a \geq 0$ has a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ , and $a^{1 / 2} = \sqrt{a}$ ; the base $0$ is covered, with $0^{r} = 0$ for rational $r > 0$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Rational powers $a^{r}$ of a positive base, Order on the rationals).

[L2]

For $a, b \geq 0$ : $a \leq b$ if and only if $a^{2} \leq b^{2}$ ; and squares are nonnegative (Squaring is monotone on the nonnegatives, Squares of nonzero elements are positive).

[L3]

Rational power laws for a positive base: $a^{r} > 0$ , $a^{r + s} = a^{r} a^{s}$ , $a^{- r} = 1 / a^{r}$ , $(a^{r})^{s} = a^{r s}$ , and $(a b)^{r} = a^{r} b^{r}$ (Laws of rational exponents).

[L4]

Monotonicity in the base: for rational $r > 0$ and $0 < a < b$ one has $a^{r} < b^{r}$ (Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ ).

[L5]

Archimedean property: for every real $t$ there is a natural $n \geq 1$ with $t < n$ ; and $0 < a < b$ gives $0 < 1 / b < 1 / a$ (Every complete ordered field is Archimedean, For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Inverses of positives are positive, and reciprocation reverses order).

[L6]

The absolute value and its properties, and the usual metric of $R$ (Basic properties of the absolute value, The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, Sign rules for products and monotonicity of multiplication).

[L7]

A Hölder map is uniformly continuous (Contraction implies Lipschitz implies uniformly continuous implies continuous; every Hölder map is uniformly continuous, and a Lipschitz map on a bounded space is Hölder for every exponent).

Verification

technique · direct

1.1

Both sides of the inequality of claim 1 are symmetric in $x$ and $y$ , so it is enough to prove it when $x \geq y \geq 0$ ; then $\sqrt{x} \geq \sqrt{y}$ and $∣ x - y ∣ = x - y$ .

L2L6

1.2

Claim 4: let $α$ be rational with $1 / 2 < α \leq 1$ , put $β : = α - 1 / 2$ , a positive rational, and suppose $∣ \sqrt{x} - \sqrt{y} ∣ \leq C ∣ x - y ∣^{α}$ for all $x, y \geq 0$ with some real $C \geq 0$ . Taking $y = 0$ gives $t^{1 / 2} \leq C t^{α}$ for every real $t > 0$ .

L1L3L5

2.1

With $x \geq y \geq 0$ put $u : = \sqrt{y} + \sqrt{x - y} \geq 0$ . Then $u^{2} = y + 2 \sqrt{y} \sqrt{x - y} + (x - y) = x + 2 \sqrt{y} \sqrt{x - y} \geq x$ , the added term being a product of nonnegatives.

step 1.1L1L2

2.2

At $t = 1$ this reads $1 \leq C$ , so $C > 0$ ; and dividing the inequality of step 1.2 by $t^{α} > 0$ gives $t^{1 / 2 - α} = t^{- β} = 1 / t^{β} \leq C$ , hence $t^{β} \geq 1 / C$ for every real $t > 0$ .

step 1.2L3L5

3.1

Since $u \geq 0$ , $\sqrt{x} \geq 0$ and $(\sqrt{x})^{2} = x \leq u^{2}$ , we get $\sqrt{x} \leq u = \sqrt{y} + \sqrt{x - y}$ , hence $∣ \sqrt{x} - \sqrt{y} ∣ = \sqrt{x} - \sqrt{y} \leq \sqrt{x - y} = ∣ x - y ∣^{1 / 2}$ . This is claim 1, with Hölder constant $1$ and exponent $1 / 2$ .

step 1.1step 2.1L1L2

3.2

Apply this at $t = 1 / n$ for a natural $n \geq 1$ : $(1 / n)^{β} = 1 / n^{β}$ , so $1 / n^{β} \geq 1 / C$ and therefore $n^{β} \leq C$ for every $n \geq 1$ .

step 2.2L3L5

4.1

By [L7] a $1 / 2$ -Hölder map is uniformly continuous, so $g$ is uniformly continuous: claim 2.

step 3.1L7

4.2

Claim 3: suppose $∣ \sqrt{x} - \sqrt{y} ∣ \leq C ∣ x - y ∣^{1 / 2}$ for all $x, y \geq 0$ . Taking $y = 0$ and $x = 1$ gives $1 = \sqrt{1} \leq C \cdot 1^{1 / 2} = C$ , so $C \geq 1$ .

step 3.1L1L3

5.1

But $C > 0$ , so $C^{1 / β}$ is a positive real and [L5] supplies a natural $n \geq 1$ with $n > C^{1 / β}$ ; raising to the positive rational power $β$ gives $n^{β} > (C^{1 / β})^{β} = C$ , contradicting step 3.2. So no such $C$ exists and $g$ is not $α$ -Hölder: claim 4, and at $α = 1$ it says $g$ is not Lipschitz.

step 2.2step 3.2L3L4L5∎

Remarks

Where the failure is located. The obstruction in claims 3 and 4 sits at $0$ : the inequality $t^{1 / 2} \leq C t^{α}$ is comfortable for large $t$ and impossible for small $t$ once $α > 1 / 2$ , because $t^{1 / 2}$ then dominates $t^{α}$ . Away from $0$ the square root is perfectly Lipschitz: on $[a, \infty)$ with $a > 0$ one has $∣ \sqrt{x} - \sqrt{y} ∣ = ∣ x - y ∣ / (\sqrt{x} + \sqrt{y}) \leq ∣ x - y ∣ / (2 \sqrt{a})$ , since $\sqrt{x} + \sqrt{y} \geq 2 \sqrt{a} > 0$ and $(\sqrt{x} - \sqrt{y}) (\sqrt{x} + \sqrt{y}) = x - y$ .
The exponent is rational, and that is not a restriction here. At this page's position in the reading order, Rational powers $a^{r}$ of a positive base is the available exponent construction. Both $1 / 2$ and every exponent used above are rational, so claim 4 is intentionally local to rational $α$ ; real powers are introduced later in Real powers for positive bases, with the zero-base positive-exponent convention ↗.
What this example is for. It is one of the two witnesses named in Contraction implies Lipschitz implies uniformly continuous implies continuous; every Hölder map is uniformly continuous, and a Lipschitz map on a bounded space is Hölder for every exponent: it shows that "Hölder" is strictly weaker than "Lipschitz", so the implication proved there from Hölder to uniform continuity is not a detour through the Lipschitz condition. The other witness, separating continuity from uniform continuity, is $x \mapsto 1 / x$ is continuous on $(0, 1)$ and sends the Cauchy sequence $(1 / (k + 2))_{k \geq 0}$ to an unbounded one.
Claim 1 is sharp in a second sense as well: equality holds whenever one of the two arguments is $0$ , since $∣ \sqrt{x} - \sqrt{0} ∣ = \sqrt{x} = ∣ x - 0 ∣^{1 / 2}$ . So the estimate is attained and not merely approached.

Depends on

Used by

x ↦ √x is a uniformly continuous bijection of [0,∞) onto itself whose inverse x ↦ x² is not uniformly continuous Counterexample

Dependency tree · two levels

53 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

Hölder condition (Wikipedia) (standard reference, not scraped)
Lipschitz continuity (Wikipedia) (standard reference, not scraped)
Nth root (Wikipedia) (standard reference, not scraped)

⋅⋅​ on [0,∞)[0,∞) is uniformly continuous and exactly 1/21/2-Hölder, and is not Lipschitz