Alphabeta Math
False statementConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16
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.

FALSE: every continuous complex-valued function on a domain has a primitive

Statement

False claim. Every continuous complex-valued function on a complex domain has a primitive.

Facts & Assumptions

Given: The punctured plane U=C{0} and f(z)=1/z.

[L1]

A complex domain is a nonempty connected open subset of C (A complex domain is a nonempty connected open subset of C).

[L2]

For dimension at least two, punctured Euclidean space is polygonally connected (For n2, the punctured space Rn{0} is polygonally connected).

[L3]

Around a positively oriented circle centred at 0, z1dz=2πi (On a positively oriented circle about a, the integral of (z-a)^m is zero for every integer m except -1, and is 2 pi i for m=-1).

[L4]

The integral of a continuous complex derivative over every closed rectifiable contour is zero (The integral of a continuous complex derivative over every closed rectifiable contour is zero).

[L5]

A continuous function on a complex domain has a primitive exactly when its closed-contour integrals vanish (For a continuous function on a complex domain, endpoint independence, zero closed-contour integrals, and existence of a primitive are equivalent).

[L6]

For complex polynomials P,Q, the set where Q0 is open and P/Q is holomorphic there (Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero).

[L7]

Complex differentiability at a point implies continuity there (Complex differentiability at a point implies continuity there).

Refutation

technique · contradiction
1.1

Apply [L6] to P=1 and Q(z)=z: it makes U open and 1/z holomorphic there, hence continuous by [L7]. The point 1 lies in U, and [L2] makes U connected, so it is a domain by [L1].

L1L2L6L7
1.2

Suppose, contrary to the desired refutation, that 1/z had a primitive on U. Then [L4] would make its integral around the unit circle zero.

assume-contraL4
2.1

But [L3] gives that integral as 2πi0, a contradiction. Hence the false claim fails, and [L5] gives the corrected zero-closed-contour criterion.

step 1.2L3L5discharge-contradiction

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: 170 results over 24 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