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

A contour missing a point subdivides into arcs lying in discs that miss it

Statement

Let $γ : [a, b] \to C$ be a complex contour with trace $γ^{*}$ and let $p \in C$ with $p \notin γ^{*}$ . Then

$d : = \inf {∣ w - p ∣ : w \in γ^{*}}$

exists and satisfies $d > 0$ , and there is $δ > 0$ with the following property: whenever $a < b$ and $a = t_{0} < t_{1} < \dots < t_{r} = b$ is a partition of $[a, b]$ of mesh smaller than $δ$ ,

$γ ([t_{i}, t_{i + 1}]) \subseteq D (γ (t_{i}), d) and p \notin D (γ (t_{i}), d) for every i < r,$

where $D (u, d)$ is the open disc of centre $u$ and radius $d$ . At least one such partition exists. If instead $a = b$ the trace is the single point $γ (a)$ , which lies in $D (γ (a), d)$ , and $p \notin D (γ (a), d)$ ; no partition is involved in that case.

Facts & Assumptions

Given: A complex contour $γ : [a, b] \to C$ and a point $p \notin γ^{*}$ ; the plane carries the Euclidean metric of $C = R [x] / (x^{2} + 1)$ as the Euclidean plane and as a normed real algebra: what the identification preserves.

[L1]

A complex contour is a rectifiable path $γ : [a, b] \to C$ , in particular a continuous map on a compact interval (Rectifiable complex contours, reversal, concatenation, closedness, and orientation).

[L2]

The continuous image of a compact subset is a compact subset (The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset).

[L3]

A compact subset of a metric space is closed and bounded (A compact subset of a metric space is closed and bounded).

[L4]

A continuous map from a compact metric space to a metric space is uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

[L5]

A subset of $R^{n}$ is compact exactly when it is closed and bounded, and closed boxes are compact (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).

[L6]

$B (x, r) = {y : d (x, y) < r}$ , and a set is open exactly when each of its points admits a ball around it inside the set, a set being closed when its complement is open (Open ball, closed ball and sphere in a metric space, 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).

[L7]

A partition of $[a, b]$ with $a < b$ consists of $a = t_{0} < \dots < t_{r} = b$ with $r \geq 1$ ; its mesh is the largest of the lengths $t_{i + 1} - t_{i}$ , and the uniform partition into $N$ parts has mesh $(b - a) / N$ (Partition of $[a, b]$ as a finite strictly increasing list $a = t_{0} < t_{1} < \dots < t_{n} = b$ , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions).

[L8]

For every real $ε > 0$ there is a natural $n \geq 1$ with $1 / n < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[L9]

A nonempty subset of $R$ bounded below has a greatest lower bound (Every nonempty set bounded below has an infimum, Greatest lower bound (infimum)).

Proof

technique · direct

1.1givenL1L2L3L5

By [L1] and [L5] the parameter interval is compact and $γ$ is continuous, so $γ^{*}$ is a nonempty compact subset of $C$ by [L2], and it is closed by [L3].

1.2givenL1L4L5

By [L1] and [L5] again, $γ$ is uniformly continuous on $[a, b]$ by [L4].

2.1step 1.1L6L9

The set ${∣ w - p ∣ : w \in γ^{*}}$ is nonempty and bounded below by $0$ , so $d$ exists by [L9]. Since $p \notin γ^{*}$ and $γ^{*}$ is closed by step 1.1, its complement is open, so [L6] gives $ε > 0$ with $B (p, ε) \cap γ^{*} = \emptyset$ , that is $∣ w - p ∣ \geq ε$ for every $w \in γ^{*}$ ; hence $d \geq ε > 0$ .

3.1step 1.2step 2.1choose

Apply the uniform continuity of step 1.2 with the positive number $d$ of step 2.1: there is $δ > 0$ such that $∣ γ (t) - γ (s) ∣ < d$ whenever $s, t \in [a, b]$ satisfy $∣ t - s ∣ < δ$ .

4.1step 2.1step 3.1L6L7

Let $a < b$ and let $a = t_{0} < \dots < t_{r} = b$ have mesh below $δ$ . For $i < r$ and $t \in [t_{i}, t_{i + 1}]$ one has $∣ t - t_{i} ∣ \leq t_{i + 1} - t_{i} < δ$ , so $∣ γ (t) - γ (t_{i}) ∣ < d$ by step 3.1 and hence $γ (t) \in D (γ (t_{i}), d)$ by [L6]; and $∣ p - γ (t_{i}) ∣ \geq d$ by step 2.1, since $γ (t_{i}) \in γ^{*}$ , so $p \notin D (γ (t_{i}), d)$ .

5.1step 2.1step 4.1L6L7L8∎

Such a partition exists when $a < b$ : by [L8] applied to $δ / (b - a)$ there is a natural $N \geq 1$ with $(b - a) / N < δ$ , and the uniform partition into $N$ parts has mesh $(b - a) / N < δ$ by [L7]. If $a = b$ then $γ^{*} = {γ (a)}$ , which lies in $D (γ (a), d)$ because $d > 0$ , while $∣ p - γ (a) ∣ \geq d$ keeps $p$ out of that disc.

Depends on

Used by

Dependency tree · two levels

67 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, Exercise 1 (standard reference, not scraped)