LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22

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.

Banach-valued Cauchy integral vanishes

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $A$ be a unital complex Banach algebra, let $U \subseteq C$ be open, and let $F : U \to A$ be continuous and weakly holomorphic: for every bounded linear functional $φ : A \to C$ (The dual space X^* of a normed space and its dual norm) the scalar function $φ \circ F : U \to C$ is holomorphic. Let $Γ$ be a complex chain which is a cycle, with trace in $U$ (Complex chains, their traces, and cycles) and null-homologous in $U$ (Null-homologous cycles and homologous cycles in an open set). Then

$\int_{Γ} F (z) d z = 0,$

the integral being that of Banach algebra valued contour integral over the chain $Γ$ . The Axiom of Choice is used exactly once, in the separation step supplied by The dual space separates points of a normed space.

Facts & Assumptions

Given: An assumed Axiom of Choice, an open $U \subseteq C$ , a continuous weakly holomorphic $F : U \to A$ , and a chain $Γ = \sum_{k < r} m_{k} γ_{k}$ which is a cycle with trace $Γ^{*} \subseteq U$ and is null-homologous in $U$ .

[F1]

For $p \notin Γ^{*}$ one has $\int_{Γ} d z / (z - p) = 2 π i n (Γ, p)$ , and $\int_{Γ} g d z = \sum_{\begin{array}{c} k < r \\ m_{k} \neq 0 \end{array}} m_{k} \int_{γ_{k}} g d z$ for every $g$ continuous on $Γ^{*}$ ; integrals over chains are additive (Banach algebra valued contour integral, Integration over a complex chain and the index of a chain).

[F2]

For a bounded linear $φ : A \to C$ and a single contour $γ$ , bounded linearity commutes with the contour integral (Contour integral commutes with bounded linear maps). Hence for the finite chain $Γ = \sum_{k < r} m_{k} γ_{k}$ and every $f$ continuous on its trace, $φ ⁣ (\int_{Γ} f d z) = \sum_{\begin{array}{c} k < r \\ m_{k} \neq 0 \end{array}} m_{k} φ ⁣ (\int_{γ_{k}} f d z) = \int_{Γ} (φ \circ f) d z,$ by the chain-integral definition in [F1]. Each retained contour has trace contained in $Γ^{*}$ , so its integral is defined; zero-coefficient contours are omitted even if their traces lie outside the domain of $f$ . For an empty retained list, both sides are zero by linearity.

[F3]

If $Ω \subseteq C$ is open, $g : Ω \to C$ is holomorphic, and $Γ$ is a complex chain which is a cycle with trace in $Ω$ and null-homologous in $Ω$ , then $\int_{Γ} g d z = 0$ (Cauchy's theorem for a null-homologous cycle).

[F4]

If $x \neq y$ in a complex normed space $V$ then there is a bounded linear functional $φ$ on $V$ with $φ (x) \neq φ (y)$ (The dual space separates points of a normed space).

[A1]

The standing hypothesis is the Axiom of Choice, used here through [F4] and nowhere else (The Axiom of Choice).

Proof

technique · direct

1.1

For every bounded linear functional $φ : A \to C$ the composition $φ \circ F$ is holomorphic on $U$ by weak holomorphy, and it is continuous; moreover $Γ$ is a cycle with trace in $U$ that is null-homologous in $U$ by hypothesis, so [F3] applies to $g : = φ \circ F$ and gives $\int_{Γ} φ (F (z)) d z = 0$ .

F1F3

2.1

For every bounded linear $φ$ , $φ (\int_{Γ} F d z) = \int_{Γ} φ (F (z)) d z = 0$ : the first equality is [F2], and the second is [step 1.1].

step 1.1F2

3.1

Suppose $\int_{Γ} F d z \neq 0$ . Then [F4] applied to the distinct points $x : = \int_{Γ} F d z$ and $0$ produces a bounded linear functional $φ$ with $φ (\int_{Γ} F d z) \neq 0$ , contradicting [step 2.1]; hence $\int_{Γ} F d z = 0$ .

step 2.1F4A1∎

Depends on

Used by

Riesz spectral projection Definition
Holomorphic functional calculus is contour independent Lemma

Dependency tree · two levels

49 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

Theo Bühler and Dietmar A. Salamon, Functional Analysis — Lemma 5.11 and Theorem 5.25(i), printed pp. 217–219 and 228 (standard reference, not scraped)
Vahid Shirbisheh, Lectures on C-star Algebras, v2 — §2.5, printed pp. 43–47 (standard reference, not scraped)