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.

$∣ x ∣$ is Lipschitz and absolutely continuous but not $C^{1}$ on $[- 1, 1]$

Example

The absolute-value function separates two implications in the hierarchy: it is Lipschitz, hence absolutely continuous, but is not even differentiable at the origin.

Facts & Assumptions

Given: The function $f (x) = ∣ x ∣$ on $[- 1, 1]$ .

[L1]

The reverse triangle inequality gives $∣ ∣ x ∣ - ∣ y ∣ ∣ \leq ∣ x - y ∣$ (The reverse triangle inequality).

[L2]

Every Lipschitz function on a compact interval is absolutely continuous ( $C^{1}$ implies Lipschitz, Lipschitz implies absolutely continuous, and absolutely continuous implies continuous and bounded variation).

[L3]

Differentiability requires a two-sided difference-quotient limit (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).

Verification

technique · direct

1.1

By [L1], $f$ is $1$ -Lipschitz, and [L2] makes it absolutely continuous.

L1L2

2.1

At zero, $(∣ h ∣ - ∣ 0 ∣) / h$ equals $1$ for $h > 0$ and $- 1$ for $h < 0$ . The two one-sided limits differ, so [L3] shows that $f^{'} (0)$ does not exist. Therefore $f$ is not $C^{1}$ on $[- 1, 1]$ .

L3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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)

∣x∣∣x∣ is Lipschitz and absolutely continuous but not C1C1 on [−1,1][−1,1]