ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-08-11

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{x}$ is absolutely continuous but not Lipschitz on $[0, 1]$

Example

The function $f (x) = \sqrt{x}$ is absolutely continuous on $[0, 1]$ , although its slope near zero prevents any global Lipschitz constant.

Facts & Assumptions

Given: $f (x) = \sqrt{x}$ on $[0, 1]$ .

[L1]

Nonnegative square roots exist, are unique, and are increasing (Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ , Squaring is monotone on the nonnegatives).

[L2]

Absolute continuity is tested on finite disjoint families of intervals (Absolute continuity on a compact interval).

[L3]

A Lipschitz bound must hold for every pair of points (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction).

Verification

technique · direct

1.1

Let $[u_{j}, v_{j}]$ be pairwise nonoverlapping subintervals. Fix $r > 0$ and split at $r$ the one family interval, if any, that crosses $r$ ; monotonicity makes this split preserve its endpoint increment. The resulting pieces contained in $[0, r]$ contribute at most $\sqrt{r}$ in total, because their increments telescope after gaps are filled. On every remaining interval, whose left endpoint satisfies $u_{j} \geq r$ , [given] $\sqrt{v_{j}} - \sqrt{u_{j}} = \frac{v_{j} - u_{j}}{\sqrt{v_{j}} + \sqrt{u_{j}}} \leq \frac{v_{j} - u_{j}}{2 \sqrt{r}} .$

1.2

Given $ε > 0$ , choose $r > 0$ with $\sqrt{r} < ε / 2$ , then require $\sum_{j} (v_{j} - u_{j}) < ε \sqrt{r}$ . Steps 1.1 and 1.2 make the total endpoint increment less than $ε$ , proving absolute continuity by [L2].

L1L2

2.1

If a Lipschitz constant $K$ existed, the pair $0$ and $1 / n^{2}$ would give $n^{- 1} \leq K n^{- 2}$ , hence $n \leq K$ for every positive integer $n$ , contradicting the Archimedean property. Thus [L3] fails.

L3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

34 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

Christopher Heil, Absolute Continuity and the Banach-Zaretsky Theorem, Section 2 (standard reference, not scraped)

xx​ is absolutely continuous but not Lipschitz on [0,1][0,1]