CounterexampleConstruction: Literature-sourcedVerification: Literature-sourcedSession-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 ∣^{2}$ is complex differentiable exactly at $0$ , with derivative $0$ , but is holomorphic on no neighbourhood of $0$

Statement refuted

Complex differentiability at a point automatically extends to holomorphy on some neighbourhood of that point.

Facts & Assumptions

Given: $f (z) = ∣ z ∣^{2} = z \overset{ˉ}{z}$ on $C$ .

[L1]

Complex differentiability at a point is existence of the difference-quotient limit, while holomorphy at a point requires complex differentiability on an open neighbourhood of that point (Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions).

[L2]

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

[L3]

$∣ z ∣^{2} = z \overset{ˉ}{z}$ , $\overline{\overline{z}} = z$ , 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). Since $\overline{\overline{z}} = z$ and $z \overline{z} = ∣ z ∣^{2}$ , one has $∣ \overline{z} ∣^{2} = \overline{z} \overline{\overline{z}} = \overline{z} z = ∣ z ∣^{2}$ , and both moduli are nonnegative, so $∣ \overline{z} ∣ = ∣ z ∣$ .

Counterexample

technique · cases

1.1

At $z = 0$ and $h \neq 0$ , $\frac{f (h) - f (0)}{h} = \frac{∣ h ∣^{2}}{h} = \overset{ˉ}{h},$ whose modulus is $∣ h ∣$ and hence tends to $0$ . Thus $f^{'} (0) = 0$ .

L1L3assume-case zero

1.2

At $z = x + i y$ , the components are $u = x^{2} + y^{2}$ and $v = 0$ , so $u_{x} = 2 x$ , $u_{y} = 2 y$ , and $v_{x} = v_{y} = 0$ .

algebra

2.1

If $f$ were complex differentiable at a nonzero $z$ , [L2] would force $2 x = 0$ and $2 y = 0$ , hence $z = 0$ , a contradiction. Therefore $f$ is not complex differentiable at any nonzero point.

step 1.2L2assume-case nonzeroalgebra

3.1

Steps 1.1 and 2.1 cover every $z \in C$ , so the complex-differentiability locus is exactly ${0}$ . Every open neighbourhood of $0$ contains a nonzero point, where step 2.1 gives failure; thus [L1] says $f$ is holomorphic on no neighbourhood of $0$ .

step 1.1step 2.1L1L3cases-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: 51 results over 14 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, Exercise 2.1.3 (standard reference, not scraped)

z↦∣z∣2z↦∣z∣2 is complex differentiable exactly at 00, with derivative 00, but is holomorphic on no neighbourhood of 00