Alphabeta Math
False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck 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 n≥2, the punctured space Rn∖{0} is polygonally connected).

[L3]

Around a positively oriented circle centred at 0, ∫z−1 dz=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 Q≠0 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.1L1L2L6L7

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

1.2assume-contraL4

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.

2.1step 1.2L3L5discharge-contradiction∎

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

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

33 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources