LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 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 bisection selects nested triangles retaining one quarter of the boundary-integral magnitude, with halving diameters and a one-point intersection

Statement

Let $U \subseteq C$ be open, let $f : U \to C$ be continuous, and let $T_{0} = Δ [a, b, c] \subseteq U$ . There is a sequence $(T_{n})_{n \in N}$ of filled triangles such that $T_{n + 1}$ is one of the four midpoint subtriangles of $T_{n}$ and, for every $n \in N$ ,

$T_{n + 1} \subseteq T_{n}, ∣ I_{f} (T_{n}) ∣ \geq 4^{- n} ∣ I_{f} (T_{0}) ∣,$

$P (T_{n}) = 2^{- n} P (T_{0}), diam (T_{n}) = 2^{- n} diam (T_{0}) .$

Every $T_{n}$ is nonempty, compact, closed, and bounded, and there is a unique $z_{*} \in C$ with

$⋂_{n \in N} T_{n} = {z_{*}} .$

Here $I_{f} (T)$ denotes the integral over the oriented boundary prescribed by Filled complex triangles, their oriented three-edge boundary contours, diameter, and perimeter.

Facts & Assumptions

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

[L1]

The four midpoint subtriangle boundary integrals sum to the parent boundary integral (Midpoint subdivision of a triangle cancels every interior edge and preserves its outer boundary integral).

[L2]

In a metric space, pairwise distances inside a nonempty bounded set are at most its diameter; Cauchy sequences and convergence are tested by positive real tolerances; the complement of a closed set is open; and distance zero forces equality (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Cauchy sequence in a metric space, Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ , The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

[L3]

The complex plane with its usual metric is complete (The complex plane is complete, and convergence is equivalent to convergence of real and imaginary parts).

[L4]

The unit square in $R^{2}$ is compact, a continuous image of a compact metric space is compact, and a compact subset of a metric space is closed and bounded (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset, A compact subset of a metric space is closed and bounded).

[L5]

Recursion constructs a sequence from an initial value and a self-map; every nonempty set of natural numbers has a least element; induction proves a statement for all natural indices (The recursion theorem, The well-ordering principle, The principle of mathematical induction).

[L6]

If $0 < r < 1$ , then the real sequence $(r^{n})$ tends to zero (For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ ).

[L7]

The complex modulus satisfies the triangle inequality $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

Proof

technique · direct

1.1L1L5L7

For any parent triangle, [L1] and [L7] imply that at least one of its four indexed midpoint children has integral modulus at least one quarter of the parent's: otherwise the modulus of their sum would be strictly smaller than the parent modulus. Choose the least qualifying index, which also works when the parent integral is zero.

1.2L4algebra

If $T_{n} = Δ [u, v, w]$ , the continuous map $Φ (s, t) = u + s ((1 - t) (v - u) + t (w - u))$ takes the compact square $[0, 1]^{2}$ onto $T_{n}$ : its coefficients are nonnegative and sum to one, and conversely a barycentric point with coefficients $(α, β, γ)$ is obtained by $s = β + γ$ and, when $s > 0$ , $t = γ / s$ , while $s = 0$ gives $u$ . Thus [L4] makes $T_{n}$ compact, closed, and bounded; it is nonempty because it contains $u$ .

2.1step 1.1L5algebra

The least-index rule is a function of the ordered parent triangle, so recursion gives $(T_{n})$ ; direct midpoint geometry shows every child is contained in its parent and is the image of it under a similarity of ratio $1 / 2$ , hence its perimeter and diameter are half those of the parent.

3.1step 1.1step 2.1L5

Induction applied to step 2.1 and the retained one-quarter estimate gives, including at $n = 0$ , $∣ I_{f} (T_{n}) ∣ \geq 4^{- n} ∣ I_{f} (T_{0}) ∣$ , $P (T_{n}) = 2^{- n} P (T_{0})$ , and $diam (T_{n}) = 2^{- n} diam (T_{0})$ .

4.1step 2.1step 3.1step 1.2L2L3L6∎

By [L6] and step 3.1, the diameters tend to zero, even when the initial diameter is zero. Write $v_{n}$ for the first listed vertex of the ordered triangle $T_{n}$ ; this is determined by the recursive construction and makes no choice. If $m, n \geq N$ , then $v_{m}, v_{n} \in T_{N}$ by nestedness, so $∣ v_{m} - v_{n} ∣ \leq diam (T_{N})$ . Thus $(v_{n})$ is Cauchy and [L3] gives a limit $z_{*} \in C$ . For fixed $N$ , the tail $(v_{n})_{n \geq N}$ lies in the closed set $T_{N}$ . If $z_{*} \notin T_{N}$ , its open complement would contain a ball about $z_{*}$ , contradicting convergence of that tail; hence $z_{*} \in T_{N}$ . Therefore $z_{*}$ lies in every $T_{N}$ . If $w$ is another common point, then $w, z_{*} \in T_{N}$ gives $∣ w - z_{*} ∣ \leq diam (T_{N})$ for every $N$ ; since these diameters tend to zero, $∣ w - z_{*} ∣ = 0$ and $w = z_{*}$ . Hence the intersection is exactly ${z_{*}}$ .

Depends on

Used by

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

Dependency tree · two levels

87 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

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