Session-authored (Fable 5 assisted)

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.

✓ 6 results · all verified · 5 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Hartogs Phenomena — Examples

1 · Prerequisites

2 · Summary

These examples isolate the geometric and algebraic faces of the Hartogs phenomena. The first two make the Hartogs figure concrete and show that the extension theorem is not merely existential: familiar rational functions already extend across the missing core. The next example turns the puncture theorem into a visible computation on the bidisc minus the origin.

The two counterexamples mark the sharp boundary. In one variable, $1 / z$ really has a nonremovable puncture, so the dimension hypothesis $m \geq 2$ is essential. And removing a complex hypersurface behaves differently from removing a compact hole: $C^{2} ∖ {z_{1} = 0}$ supports the holomorphic obstruction $1 / z_{1}$ , so it remains a domain of holomorphy.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

The Hartogs figure in (|z1|, |z2|) coordinates

Example

For $0 < r, s < 1$ , the Hartogs figure $H (r, s)$ is the union of a thin inner cylinder and a thick outer shell:

H (r, s) = {∣ z_{1} ∣ < 1, ∣ z_{2} ∣ < s} \cup {r < ∣ z_{1} ∣ < 1, ∣ z_{2} ∣ < 1} .

In the $(∣ z_{1} ∣, ∣ z_{2} ∣)$ -plane this is exactly the region obtained by taking the rectangle $[0, 1) \times [0, s)$ together with the vertical strip $(r, 1) \times [0, 1)$ .

Facts & Assumptions

Given: Real numbers $0 < r, s < 1$ .

[L1]

The Hartogs figure and its bidisc hull are defined by the displayed modulus conditions in the two coordinates (The Hartogs figure H(r,s) and its bidisc hull).

Verification

technique · direct

1.1

By [L1], membership in $H (r, s)$ depends only on the two moduli $∣ z_{1} ∣$ and $∣ z_{2} ∣$ , and the two defining pieces are exactly the inequalities listed in the Example.

2.1

So the picture in modulus coordinates is the union of the thin horizontal rectangle $[0, 1) \times [0, s)$ with the outer vertical strip $(r, 1) \times [0, 1)$ , while the missing core is $[0, r] \times [s, 1)$ .

step 1.1∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

The function 1 / (1 - z1 z2) extends holomorphically from a Hartogs figure

Example

The function

f (z_{1}, z_{2}) = \frac{1}{1 - z_{1} z_{2}}

is holomorphic on the full bidisc ${∣ z_{1} ∣ < 1, ∣ z_{2} ∣ < 1}$ and therefore, a fortiori, on every Hartogs figure inside that bidisc.

Facts & Assumptions

Given: The function $f (z_{1}, z_{2}) = 1 / (1 - z_{1} z_{2})$ on the unit bidisc.

[L1]

Every holomorphic function on a Hartogs figure extends uniquely to the full bidisc hull (A holomorphic function on a Hartogs figure extends to the full bidisc).

Verification

technique · direct

1.1

On the unit bidisc one has $∣ z_{1} z_{2} ∣ < 1$ , so $1 - z_{1} z_{2} \neq 0$ . Hence the reciprocal $f (z_{1}, z_{2}) = 1 / (1 - z_{1} z_{2})$ is holomorphic there.

givenalgebra

2.1

Restricting $f$ to any Hartogs figure produces a concrete instance of [L1], and the extension theorem recovers the same global formula on the whole bidisc.

step 1.1L1∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

A holomorphic function on the punctured bidisc extends across the origin

Example

On the punctured bidisc ${(z_{1}, z_{2}) : ∣ z_{1} ∣ < 1, ∣ z_{2} ∣ < 1} ∖ {(0, 0)}$ , the function

f (z_{1}, z_{2}) = \frac{z_{1}}{1 - z_{1} z_{2}}

is holomorphic and extends holomorphically across the origin as the same formula.

Facts & Assumptions

Given: The punctured bidisc and the function $f (z_{1}, z_{2}) = z_{1} / (1 - z_{1} z_{2})$ .

[L1]

In complex dimension at least two, a holomorphic function on a punctured domain extends uniquely across the puncture (An isolated puncture is removable in complex dimension at least two).

Verification

technique · direct

1.1

On the full bidisc one has $∣ z_{1} z_{2} ∣ < 1$ , so $1 - z_{1} z_{2} \neq 0$ . Therefore the same formula defines a holomorphic function on the whole bidisc, and its restriction to the punctured bidisc is the displayed $f$ .

givenalgebra

2.1

This explicit extension agrees with the abstract existence statement of [L1] for the missing point $(0, 0)$ .

step 1.1L1∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

The bidisc minus the origin is not a domain of holomorphy

Example

The punctured bidisc

Ω = {(z_{1}, z_{2}) : ∣ z_{1} ∣ < 1, ∣ z_{2} ∣ < 1} ∖ {(0, 0)}

is not a domain of holomorphy.

Facts & Assumptions

Given: The punctured bidisc $Ω$ .

[L1]

A holomorphic function on a punctured several-variable domain extends across the missing point (An isolated puncture is removable in complex dimension at least two).

[L2]

A domain of holomorphy is one for which no single larger overlap works for every holomorphic function (Holomorphic extension and domains of holomorphy in several variables).

Verification

technique · direct

1.1

Let $f \in O (Ω)$ . By [L1], $f$ extends holomorphically across the missing origin to the full bidisc. So the same larger domain works for every holomorphic function on $Ω$ .

2.1

The fixed overlap can be taken to be any small bidisc around a point of $Ω$ and the larger domain is the whole bidisc. By [L2], this shows that $Ω$ is not a domain of holomorphy.

step 1.1L2∎

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

The one-variable function 1 / z does not extend across the origin

Statement refuted

Refuted claim: the one-variable function $1 / z$ extends holomorphically across $0$ .

Facts & Assumptions

Given: The holomorphic function $f (z) = 1 / z$ on $0 < ∣ z ∣ < 1$ .

[L1]

A simple pole is a pole of order $1$ (Simple poles).

[L2]

A pole is exactly a nonremovable singularity whose reciprocal has a zero at the singular point (Characterizations of poles).

Counterexample

technique · direct

1.1

The function $f (z) = 1 / z$ satisfies $z f (z) = 1$ , so $0$ is a pole of order $1$ , that is, a simple pole, by [L1].

givenL1algebra

2.1

By [L2], a pole is not removable. Hence $1 / z$ does not extend holomorphically across $0$ . This is the one-variable contrast to the several-variable puncture theorem.

step 1.1L2∎

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-27Open item page →

C^2 minus a complex line is a domain of holomorphy

Statement refuted

Refuted claim: removing a complex line from $C^{2}$ produces a domain that still cannot be a domain of holomorphy.

Facts & Assumptions

Given: The domain $Ω = {(z_{1}, z_{2}) \in C^{2} : z_{1} \neq 0}$ .

[L1]

A domain of holomorphy is tested by whether every holomorphic function extends through one fixed larger overlap (Holomorphic extension and domains of holomorphy in several variables).

Counterexample

technique · direct

1.1

The function $f (z_{1}, z_{2}) = 1 / z_{1}$ is holomorphic on $Ω$ .

givenalgebra

2.1

If $f$ extended holomorphically across any point of the missing hyperplane ${z_{1} = 0}$ , then $z_{1} f$ would extend holomorphically there as the constant function $1$ , forcing $f = 1 / z_{1}$ near that point and hence forcing a holomorphic function equal to $1 / z_{1}$ at $z_{1} = 0$ , which is impossible. So the missing complex line blocks extension, and $Ω$ is a domain of holomorphy rather than a Hartogs hole.

step 1.1L1algebra∎

The Hartogs Phenomena — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

The Hartogs figure in (|z1|, |z2|) coordinates

Example

Facts & Assumptions

Verification

The function 1 / (1 - z1 z2) extends holomorphically from a Hartogs figure

Example

Facts & Assumptions

Verification

A holomorphic function on the punctured bidisc extends across the origin

Example

Facts & Assumptions

Verification

The bidisc minus the origin is not a domain of holomorphy

Example

Facts & Assumptions

Verification

The one-variable function 1 / z does not extend across the origin

Statement refuted

Facts & Assumptions

Counterexample

C^2 minus a complex line is a domain of holomorphy

Statement refuted

Facts & Assumptions

Counterexample

Sources