ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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 winding numbers of a keyhole contour about the origin and about an excluded point

Example

Let $0 < ε < R$ and put

$C_{R} (t) = R \exp (i t), C_{ε}^{-} (t) = ε \exp (- i t) (t \in [0, 2 π]),$ $σ_{1} (t) = ε + t (R - ε), σ_{2} (t) = R + t (ε - R) (t \in [0, 1]) .$

The keyhole is the complex chain $Γ = ((1, C_{R}), (1, C_{ε}^{-}), (1, σ_{1}), (1, σ_{2}))$ . Then $Γ$ is a cycle, its trace is

$Γ^{*} = {∣ z ∣ = R} \cup {∣ z ∣ = ε} \cup {x \in R : ε \leq x \leq R},$

and at every point $z$ off that trace

$n (Γ, z) = {\begin{cases} 0, & ∣ z ∣ < ε, \\ 1, & ε < ∣ z ∣ < R, \\ 0, & ∣ z ∣ > R . \end{cases}$

The two radial segments have the same trace and both carry coefficient $1$ , so the closed segment from $ε$ to $R$ on the real axis belongs to $Γ^{*}$ and no index is asserted at any of its points.

Facts & Assumptions

Given: Reals $0 < ε < R$ and the four contours above forming the chain $Γ$ .

[L1]

The trace of a sum of chains is the union of their traces, a sum of cycles is a cycle, and for $q$ off the traces involved $n (Γ_{1} + Γ_{2}, q) = n (Γ_{1}, q) + n (Γ_{2}, q)$ and $n (Γ^{-}, q) = - n (Γ, q)$ , where $Γ^{-}$ reverses every contour (Chain integration and the index are additive in the chain, and reverse with it).

[L2]

For $a \in C$ , $r > 0$ and $k \in Z$ , the contour $γ_{k} (t) = a + r \exp (i k t)$ on $[0, 2 π]$ is a closed complex contour with $n (γ_{k}, z) = k$ for $∣ z - a ∣ < r$ and $n (γ_{k}, z) = 0$ for $∣ z - a ∣ > r$ ; for $k \neq 0$ its trace is ${z : ∣ z - a ∣ = r}$ (A circle traversed $k$ times has winding number $k$ inside and $0$ outside).

[L3]

A complex chain is a finite list of pairs $(m_{k}, γ_{k})$ ; its boundary is $\partial Γ (q) = \sum {m_{k} : γ_{k} (b_{k}) = q} - \sum {m_{k} : γ_{k} (a_{k}) = q}$ ; it is a cycle when that vanishes identically; and a list of closed contours is a cycle (Complex chains, their traces, and cycles).

[L4]

$n (Γ, q) = (2 π i)^{- 1} \int_{Γ} d z / (z - q)$ for $q$ off the trace, and for a single closed contour with coefficient $1$ this is that contour's winding number (Integration over a complex chain and the index of a chain).

[L5]

The reversal of $γ : [a, b] \to C$ is $γ^{-} (t) = γ (a + b - t)$ , and it is again a complex contour with the same trace (Reversal negates and concatenation adds winding numbers, Rectifiable complex contours, reversal, concatenation, closedness, and orientation).

[L6]

For $p \in C$ and $0 < r_{1} < r_{2}$ , the chain $C_{2} - C_{1}$ built from the positively oriented circles of radii $r_{1}, r_{2}$ about $p$ has index $0$ for $∣ z - p ∣ < r_{1}$ , $1$ for $r_{1} < ∣ z - p ∣ < r_{2}$ and $0$ for $∣ z - p ∣ > r_{2}$ (The boundary cycle of a round annulus has index $1$ inside the annulus and $0$ on either side).

[L7]

A continuous path differentiable with a continuous derivative on each piece of a partition is rectifiable (A continuous piecewise- $C^{1}$ path is rectifiable and its length is the sum of the speed integrals over its pieces).

Verification

technique · direct

1.1

The segments $σ_{1}, σ_{2}$ are affine, hence rectifiable by [L7], with $σ_{1} (0) = ε$ , $σ_{1} (1) = R$ , $σ_{2} (0) = R$ , $σ_{2} (1) = ε$ , and both have trace the closed real segment from $ε$ to $R$ ; the two circles are closed complex contours by [L2], with traces ${∣ z ∣ = R}$ and ${∣ z ∣ = ε}$ .

givenL2L7

1.2

$σ_{2}$ is the reversal of $σ_{1}$ : $σ_{1}^{-} (t) = σ_{1} (1 - t) = ε + (1 - t) (R - ε) = R + t (ε - R) = σ_{2} (t)$ , so by [L1] and [L5] the one-term chains $((1, σ_{1}))$ and $((1, σ_{2}))$ have indices summing to $0$ at every point off the segment.

givenL1L5

2.1

$Γ$ is a cycle: by [L3] the two closed circles contribute nothing to $\partial Γ$ , while $σ_{1}$ contributes $+ 1$ at $R$ and $- 1$ at $ε$ and $σ_{2}$ contributes $+ 1$ at $ε$ and $- 1$ at $R$ , so every value of $\partial Γ$ is $0$ . Its trace is the union named in the statement, by step 1.1 and [L1].

step 1.1L1L3

3.1

For $z \notin Γ^{*}$ , [L1] and [L4] split the index into the four one-term contributions, of which the two segment terms cancel by step 1.2; so $n (Γ, z) = n (C_{R}, z) + n (C_{ε}^{-}, z)$ , which by [L2] is $1 + (- 1) = 0$ for $∣ z ∣ < ε$ , $1 + 0 = 1$ for $ε < ∣ z ∣ < R$ , and $0 + 0 = 0$ for $∣ z ∣ > R$ . The same three values are what [L6] gives for the annulus cycle built from the positively oriented circles of radii $ε$ and $R$ about $0$ ; that chain is a different list from $Γ$ , and what is asserted here is only that the two index functions agree off the traces.

step 1.2step 2.1L1L2L4L6∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

53 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. V. Ahlfors, Complex Analysis, 3rd ed., Ch. 4 §2.1 (standard reference, not scraped)