LemmaStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

The complex derivative at a point is unique

Statement

If the complex derivative of $f : U \to C$ at $a \in U$ exists, its value is unique.

Facts & Assumptions

Given: An open set $U \subseteq C$ , a point $a \in U$ , and two complex numbers $L, M$ to which the difference quotient $(f (a + h) - f (a)) / h$ converges as $h \to 0$ through nonzero increments with $a + h \in U$ .

[F1]

Complex differentiability at $a$ means that the limit of $(f (a + h) - f (a)) / h$ exists as $h \to 0$ through nonzero increments with $a + h \in U$ (Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions).

[L1]

For every $z, w \in C$ , $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ , and $∣ z ∣ = 0$ if and only if $z = 0$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

Proof

technique · contradiction

1.1

Suppose, for contradiction, that $L \neq M$ , and put $ε = ∣ L - M ∣ / 3 > 0$ .

assume-contraL1

1.2

By the two asserted limits, choose $δ > 0$ such that every allowed $h$ with $0 < ∣ h ∣ < δ$ satisfies both $∣ q (h) - L ∣ < ε$ and $∣ q (h) - M ∣ < ε$ , where $q (h) = (f (a + h) - f (a)) / h$ .

givenF1choose

1.3

Since $U$ is open at $a$ , choose a nonzero allowed increment $h$ with $∣ h ∣ < δ$ .

givenchoose

2.1

The triangle inequality gives $∣ L - M ∣ \leq ∣ L - q (h) ∣ + ∣ q (h) - M ∣ < 2 ε = 2 ∣ L - M ∣ / 3$ , a contradiction. Hence $L = M$ .

step 1.1step 1.2step 1.3L1algebradischarge-contradiction∎

Depends on

Used by

Nothing in the library uses this result yet.

Cited to discharge well-definedness by Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 36 results over 11 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, §2.1.1 (standard reference, not scraped)