CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

$z \mapsto ∣ z ∣$ is nowhere complex differentiable

Statement refuted

The modulus map $z \mapsto ∣ z ∣$ is complex differentiable somewhere in $C$ .

Facts & Assumptions

Given: $f (z) = ∣ z ∣$ .

[L1]

Complex differentiability implies real total differentiability and the Cauchy–Riemann equations (Complex differentiability is equivalent to real total differentiability together with a complex-linear derivative, with $\partial_{\overset{ˉ}{z}} f = 0$ , or with the Cauchy–Riemann equations).

[L2]

$∣ z ∣^{2} = z \overset{ˉ}{z}$ , the modulus is nonnegative, and $∣ z ∣ = 0$ exactly when $z = 0$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

Counterexample

technique · cases

1.1

At $0$ , for nonzero real $t$ the difference quotient is $∣ t ∣ / t$ , which equals $1$ for $t > 0$ and $- 1$ for $t < 0$ . Thus no complex derivative exists at $0$ .

assume-case zeroL2

1.2

Let $z = x + i y \neq 0$ and put $r = ∣ z ∣ > 0$ . Rationalizing the real-coordinate increments gives $u_{x} = \lim_{t \to 0} \frac{\sqrt{(x + t)^{2} + y^{2}} - r}{t} = \lim_{t \to 0} \frac{2 x + t}{\sqrt{(x + t)^{2} + y^{2}} + r} = \frac{x}{r},$ and similarly $u_{y} = y / r$ , while the imaginary component $v$ is identically zero.

assume-case nonzeroL2algebra

2.1

If $f$ were complex differentiable at this nonzero point, [L1] would force $u_{x} = v_{y} = 0$ and $u_{y} = - v_{x} = 0$ . Step 1.2 would then give $x = y = 0$ , contradicting $z \neq 0$ .

step 1.2L1

3.1

Step 1.1 covers the origin and step 2.1 covers every nonzero point. Hence the modulus map is nowhere complex differentiable.

step 1.1step 2.1cases-exhaustive∎

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: 43 results over 12 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

J. Lebl, Guide to Cultivating Complex Analysis (standard reference, not scraped)

z↦∣z∣z↦∣z∣ is nowhere complex differentiable