TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-17

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.

Goursat's triangle theorem: a holomorphic function integrates to zero around every triangle contained in its domain

Statement

Let $U \subseteq C$ be open and let $f : U \to C$ be holomorphic. If the filled triangle $T = Δ [a, b, c]$ of Filled complex triangles, their oriented three-edge boundary contours, diameter, and perimeter is contained in $U$ , then

$\int_{\partial T} f (z) d z = 0.$

No continuity of $f^{'}$ is assumed, and repeated or collinear vertices are allowed.

Facts & Assumptions

Given: An open set $U$ , a holomorphic function $f : U \to C$ , and a filled triangle $T_{0} \subseteq U$ .

[L1]

Nested midpoint selection supplies triangles $T_{n}$ , a common point $z_{*}$ , the retention estimate $∣ I_{f} (T_{n}) ∣ \geq 4^{- n} ∣ I_{f} (T_{0}) ∣$ , and the formulas $P (T_{n}) = 2^{- n} P (T_{0})$ and $diam (T_{n}) = 2^{- n} diam (T_{0})$ (Goursat bisection selects nested triangles retaining one quarter of the boundary-integral magnitude, with halving diameters and a one-point intersection).

[L2]

If $P$ is holomorphic on an open set, $P^{'}$ is continuous there, and $γ$ is a closed rectifiable contour, then $\int_{γ} P^{'} (z) d z = 0$ (The integral of a continuous complex derivative over every closed rectifiable contour is zero).

[L3]

Complex polynomials are entire and obey the usual derivative rule (Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero).

[L4]

The ML estimate bounds the modulus of a contour integral by a bound for the integrand on the trace times the contour length (ML estimate: a contour integral is bounded by a supremum bound times path length).

[L5]

A holomorphic function is continuous (Complex differentiability at a point implies continuity there).

[L6]

Complex line integrals are linear in the integrand (Complex line integrals are linear in the integrand).

[L7]

The complex derivative at $a$ is the limit of $(f (a + h) - f (a)) / h$ as nonzero increments $h$ tend to zero within the open domain (Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions).

Proof

technique · direct

1.1

By [L5], $f$ is continuous, so [L1] gives selected triangles $T_{n}$ with common point $z_{*}$ and all the stated retention and scaling formulas.

L1L5

1.2

By [L7], differentiability at $z_{*}$ gives $f (w) = f (z_{*}) + f^{'} (z_{*}) (w - z_{*}) + (w - z_{*}) η (w)$ , where $η (w) \to 0$ as $w \to z_{*}$ ; set $η (z_{*}) = 0$ .

givenL7

1.3

Put $P (w) = f (z_{*}) w + \frac{1}{2} f^{'} (z_{*}) (w - z_{*})^{2}$ . By [L3], $P$ is entire and $P^{'} (w) = f (z_{*}) + f^{'} (z_{*}) (w - z_{*})$ is a polynomial, hence continuous. Every $\partial T_{n}$ is a closed rectifiable contour, so all hypotheses of [L2] hold and $\int_{\partial T_{n}} P^{'} (w) d w = 0$ .

L2L3

2.1

Given $ε > 0$ , take $n$ so large that $∣ η (w) ∣ < ε$ whenever $∣ w - z_{*} ∣ \leq diam (T_{n})$ ; this is possible by step 1.2 and the diameter limit in [L1]. Since $z_{*} \in T_{n}$ , [L4], [L6], and step 1.3 give $∣ I_{f} (T_{n}) ∣ \leq ε diam (T_{n}) P (T_{n})$ .

step 1.1step 1.2step 1.3L1L4L6

3.1

The retention and scaling formulas yield $∣ I_{f} (T_{0}) ∣ \leq 4^{n} ∣ I_{f} (T_{n}) ∣ \leq ε diam (T_{0}) P (T_{0})$ . Because this holds for every $ε > 0$ , $I_{f} (T_{0}) = 0$ ; the argument never divides by the initial integral, diameter, or perimeter, so it also covers zero integrals and degenerate triangles.

step 2.1L1algebra∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 147 results over 25 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

E. Stein and R. Shakarchi, Complex Analysis, Ch. 2, Theorem 1.1 (standard reference, not scraped)