TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-27

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.

Hartogs extension across a connected compact hole with a finite shell cover

Statement

Let $m \geq 2$ , let $Ω \subseteq C^{m}$ be a domain, and let $K ⋐ Ω$ be compact with $Ω ∖ K$ connected. Assume that $K$ admits a finite shell cover: there are open polydiscs $P_{1}, \dots, P_{N} \subseteq Ω$ covering $K$ such that

for each $j$ , the punctured set $P_{j} \cap (Ω ∖ K)$ contains a coordinate shell of the type treated in Hartogs figures give local extension across polydisc shells whose hull is $P_{j}$ ;
after reordering, every connected component of $P_{j} \cap ((Ω ∖ K) \cup P_{1} \cup \dots \cup P_{j - 1})$ has nonempty intersection with $Ω ∖ K$ for every $j \geq 2$ .

Then every holomorphic function on $Ω ∖ K$ extends uniquely to a holomorphic function on $Ω$ .

Facts & Assumptions

Given: A domain $Ω$ , a compact set $K ⋐ Ω$ , connected complement $Ω ∖ K$ , and a finite shell cover $P_{1}, \dots, P_{N}$ as in the Statement.

[L1]

Each coordinate shell extends holomorphically to its hull polydisc (Hartogs figures give local extension across polydisc shells).

[L2]

Local extension neighborhoods propagate along finite chains and glue uniquely (Local Hartogs extensions propagate along chains and glue uniquely).

[L3]

Holomorphic functions on connected open sets are determined by agreement on one nonempty open subset (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).

[L4]

Holomorphic extension is the overlap-agreement notion fixed on this page (Holomorphic extension and domains of holomorphy in several variables).

Proof

technique · direct

1.1

Let $f \in O (Ω ∖ K)$ . For each $j$ , the shell inside $P_{j} \cap (Ω ∖ K)$ extends to all of $P_{j}$ by [L1], so every holomorphic function on $P_{j} \cap (Ω ∖ K)$ extends holomorphically to $P_{j}$ . Assumption 1 makes $P_{1} \cap (Ω ∖ K)$ nonempty, and assumption 2 is exactly the componentwise overlap condition required by [L2]. Thus the family $(P_{j})$ satisfies the hypotheses of [L2] with $G : = Ω ∖ K$ .

L1L2given

2.1

Applying [L2] gives a holomorphic extension of $f$ from $G$ to $G \cup P_{1} \cup \dots \cup P_{N}$ . Because the polydiscs cover $K$ , this union is all of $Ω$ .

step 1.1L2

3.1

Uniqueness follows from [L3]: two extensions to $Ω$ agree on the nonempty open subset $Ω ∖ K$ , so they agree on all of the connected domain $Ω$ . The overlap language in [L4] is exactly the one used in step 1.1.

L3L4step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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

J. Lebl, Tasty Bits of Several Complex Variables, Theorem 4.3.1 (standard reference, not scraped)