ExampleConstruction: 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.

$x^{3} + 3 x y^{2} + i (y^{3} + 3 x^{2} y)$ is complex differentiable exactly on the coordinate axes but holomorphic nowhere

Example

Define $f (x + i y) = x^{3} + 3 x y^{2} + i (y^{3} + 3 x^{2} y) .$ Then $f$ is complex differentiable exactly at the points of the two coordinate axes, but it is holomorphic on no nonempty open set and hence holomorphic at no point.

Facts & Assumptions

Given: The polynomial components $u = x^{3} + 3 x y^{2}$ and $v = y^{3} + 3 x^{2} y$ on $R^{2}$ .

[L1]

If the four first partial derivatives exist near a point, are continuous at the point, and satisfy the Cauchy–Riemann equations there, then the function is complex differentiable at that point (Continuous first partial derivatives and the Cauchy–Riemann equations imply complex differentiability pointwise, and holomorphy when they hold throughout an open set).

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

Verification

technique · direct computation

1.1

The polynomial partials are continuous everywhere and satisfy $u_{x} = 3 x^{2} + 3 y^{2} = v_{y}, u_{y} = 6 x y = v_{x} .$

algebra

2.1

The second Cauchy–Riemann equation is $u_{y} = - v_{x}$ , so by step 1.1 it holds exactly when $6 x y = - 6 x y$ , equivalently $x y = 0$ .

step 1.1algebra

3.1

At every point with $x y = 0$ , [L1] and steps 1.1–2.1 give complex differentiability. At every point with $x y \neq 0$ , [L2] and step 2.1 rule it out. Thus the differentiability locus is exactly the union of the coordinate axes.

step 1.1step 2.1L1L2

4.1

Every open ball about any point of either axis contains a point with both coordinates nonzero: for radius $r > 0$ , a sufficiently small displacement in both coordinate directions supplies one. Every open ball about a point off the axes already contains its centre, where differentiability fails. Hence no nonempty open set consists entirely of differentiability points.

step 3.1

5.1

Holomorphy at a point requires complex differentiability throughout some open neighbourhood there. Step 4.1 therefore shows that $f$ is holomorphic nowhere, despite being complex differentiable at every point of both axes.

step 3.1step 4.1L1∎

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: 32 results over 9 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

Howell and Mathews, Complex Analysis, Example 3.2.9 (standard reference, not scraped)

x3+3xy2+i(y3+3x2y)x3+3xy2+i(y3+3x2y) is complex differentiable exactly on the coordinate axes but holomorphic nowhere