CorollaryStatement: AI-adaptedProof: 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.

The normalized integral around a positively oriented circle centred at a is 1

Statement

For a positively oriented circle $γ (t) = a + r \exp (i t)$ with $r > 0$ , $\frac{1}{2 π i} \int_{γ} \frac{d z}{z - a} = 1.$

Facts & Assumptions

Given: A positively oriented circle of positive radius centred at $a$ .

[L1]

The integer-monomial circle formula gives $\int_{γ} (z - a)^{- 1} d z = 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).

[L2]

The complex numbers form a field containing the embedded real field, every complex number has a unique form $a + b i$ , and every nonzero element has an inverse ( $C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ ).

[L3]

The real number $π$ is positive (Pi as twice the smallest positive zero of cosine).

Proof

technique · direct

1.1L2L3algebra

By [L3], $2 π \neq 0$ in the embedded real field; the unique complex-coordinate form in [L2] then gives $2 π i \neq 0$ , so division is licensed.

2.1step 1.1L1algebra∎

Substitute [L1] and divide to obtain $1$ . The value is independent of the positive radius, and no winding-number or Cauchy theorem is used.

Depends on

Used by

A connected plane domain that is not homologically simply connected Counterexample
A nonvanishing holomorphic function on a domain with no holomorphic logarithm Counterexample
Every cycle in a connected plane domain is null-homologous in that domain False statement
A circle traversed k times has winding number k inside and 0 outside Theorem

Dependency tree · two levels

16 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

L. Ahlfors, Complex Analysis, 3rd ed., Ch. 4 (standard reference, not scraped)