Alphabeta Math
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.

✓ 9 results · all verified · 1 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 8 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Isolated Singularities and Laurent Series — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

The same rational function has different Laurent series on different annuli

Example

The rational function

f(z)=1z(z−1)

has different Laurent series on different annuli:

1z(z−1)=−∑n≥0zn−1(0<∣z∣<1),

1z(z−1)=∑n≥0z−n−2(∣z∣>1),

and, with w=z−1,

1z(z−1)=∑n≥0(−1)n(z−1)n−1(0<∣z−1∣<1).

Each is a convergent Laurent series on its stated annulus (Convergent Laurent series on an annulus).

Facts & Assumptions

Given: The function f(z)=1/(z(z−1)).

Verification

technique · direct
1.1algebra

On 0<∣z∣<1, 1z(z−1)=−1z⋅11−z=−∑n≥0zn−1.

1.2algebra

On ∣z∣>1, 1z(z−1)=1z2⋅11−z−1=∑n≥0z−n−2.

1.3algebra

Writing w=z−1, on 0<∣w∣<1 one has 1z(z−1)=1w(1+w)=1w⋅11−(−w)=∑n≥0(−1)nwn−1.

2.1step 1.1step 1.2step 1.3∎

Since the three right-hand sides are different formal Laurent series attached to different annuli, the same rational function really does have different Laurent expansions on different annuli.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-26Open item page →

Positive powers have poles at infinity and their reciprocals have removable singularities there

Example

For every integer m≥1,

f(z)=zm

has a pole of order m at ∞, while

g(z)=1zm

has a removable singularity at ∞.

Facts & Assumptions

Given: An integer m≥1.

[L1]

A singularity at infinity is classified by the singularity of the pulled-back function h(w)=f(1/w) at w=0 (Isolated singularities at infinity).

[L2]

A pole is characterized by a finite nonzero principal part, and a removable singularity by vanishing principal part or holomorphic extendability (Characterizations of poles, Characterizations of removable singularities).

Verification

technique · direct
1.1L1L2

For f(z)=zm, the pulled-back function is f(1/w)=w−m on 0<∣w∣<1/R, so it has a pole of order m at 0 by [L2]; therefore f has a pole of order m at ∞ by [L1].

2.1L1L2∎

For g(z)=z−m, the pulled-back function is g(1/w)=wm, which is holomorphic at 0 and vanishes there; by [L2] the singularity at 0 is removable, so g has a removable singularity at ∞ by [L1].

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-26Open item page →

The residue of e^z/z^3 from the pole-derivative formula

Example

At 0, the function ez/z3 has residue 1/2.

Facts & Assumptions

Given: The function f(z)=ez/z3.

[L1]

For a pole of order m, the residue is 1(m−1)! times the (m−1)st derivative of (z−a)mf(z) at the pole (Residue formula for a pole of order m).

[L2]

The complex exponential is entire and equals its own derivative, so all derivatives of ez are again ez (The complex exponential is entire and its complex derivative is itself).

Verification

technique · direct
1.1givenalgebra

At 0, the factor z3f(z) is ez, so f has a pole of order 3 there.

2.1step 1.1L1

Applying [L1] with m=3 gives Res⁡ ⁣(ezz3,0)=12!d2dz2(ez)∣z=0.

3.1step 2.1L2algebra∎

By [L2], the second derivative of ez is still ez, so the right-hand side of step 2.1 is 12 e0=12.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-26Open item page →

A residue of p over q at a simple zero is p(a)/q'(a)

Example

For

p(z)=z+1,q(z)=z2−1,

the function p/q has a simple pole at a=1, and

Res⁡ ⁣(z+1z2−1,1)=1.

Facts & Assumptions

Given: The quotient f(z)=(z+1)/(z2−1).

[L1]

If q(a)=0 and q′(a)≠0, then Res⁡(p/q,a)=p(a)/q′(a) (Residues of p over q at a simple zero of q).

Verification

technique · direct
1.1givenalgebra

At a=1 one has q(1)=0, q′(z)=2z, and therefore q′(1)=2≠0.

2.1step 1.1L1algebra∎

Applying [L1] gives Res⁡ ⁣(z+1z2−1,1)=p(1)q′(1)=22=1.

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

Zero residue does not imply a removable singularity

Statement refuted

Refuted claim: if Res⁡(f,a)=0, then a is a removable singularity of f.

The witness is

f(z)=1z2(a=0).

Its residue at 0 is 0, but 0 is a pole of order 2, not a removable singularity.

Facts & Assumptions

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

[L1]

The residue is the coefficient of (z−a)−1 in the Laurent expansion (The residue of an isolated singularity).

[L2]

A finite nonzero principal part characterizes a pole (Characterizations of poles).

Counterexample

technique · direct
1.1L1algebra

The Laurent expansion of f at 0 is just z−2, so the coefficient of z−1 is 0; by [L1], Res⁡(f,0)=0.

2.1L2step 1.1algebra

The same Laurent expansion has finite nonzero principal part z−2, so [L2] makes 0 a pole of order 2.

3.1step 1.1step 2.1∎

Thus f has residue 0 at 0 but the singularity is not removable, refuting the claim.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-26Open item page →

e^{1/z} has an essential singularity at 0 and omits the value 0

Statement refuted

Refuted claim: an essential singularity attains every complex value on each punctured neighbourhood.

The witness is

f(z)=e1/z

at a=0. The singularity is essential, but the value 0 is omitted on every punctured neighbourhood of 0.

Facts & Assumptions

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

[L1]

Every isolated singularity is removable, a pole, or essential (Every isolated singularity is removable, a pole, or essential).

[L3]

The exponential satisfies exp⁡(u+v)=exp⁡(u)exp⁡(v) for all complex u,v (exp⁡(z+w)=exp⁡z exp⁡w, and the complex exponential extends the real exponential).

Counterexample

technique · direct
1.1L2algebra

Since z↦1/z is holomorphic on 0<∣z∣<1 and exp⁡ is entire by [L2], the function f(z)=e1/z is holomorphic on 0<∣z∣<1.

1.2L3algebra

If e1/z0=0 for some z0≠0, then [L3] gives 1=e1/z0e−1/z0=e0=0, impossible. Hence e1/z never takes the value 0.

2.1step 1.1algebra

Along the positive real axis, f(t)=e1/t→∞ as t↓0, so the singularity is not removable. Along the negative real axis, f(−t)=e−1/t→0 as t↓0, so the singularity is not a pole.

3.1step 2.1L1

By [L1], a singularity that is neither removable nor a pole is essential, so 0 is an essential singularity of e1/z.

4.1step 3.1step 1.2∎

Thus e1/z has an essential singularity at 0 and still omits the value 0, refuting the claim and showing why Casorati-Weierstrass theorem gives density rather than surjectivity.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-26Open item page →

sin(1/z) has an essential singularity at 0

Statement refuted

Refuted claim: if a holomorphic function on a punctured disc stays bounded along one approach ray to the centre, then its singularity there must be removable or a pole.

The witness is

f(z)=sin⁡(1/z)

at a=0. It stays bounded on the positive real axis but still has an essential singularity at 0.

Facts & Assumptions

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

[L1]
[L2]

Every isolated singularity is removable, a pole, or essential (Every isolated singularity is removable, a pole, or essential).

Counterexample

technique · direct
1.1givenalgebra

For t>0, one has ∣f(t)∣=∣sin⁡(1/t)∣≤1, so the function is bounded along the positive real axis approaching 0.

1.2L1algebra

For t>0, f(it)=sin⁡(−i/t)=−isinh⁡(1/t), so ∣f(it)∣=∣sinh⁡(1/t)∣→∞ as t↓0; therefore the singularity is not removable.

2.1step 1.1

Since f is bounded along the positive real axis by step 1.1, the modulus does not tend to ∞ along every approach to 0; therefore the singularity is not a pole.

3.1step 1.2step 2.1L2∎

By [L2], a singularity that is neither removable nor a pole is essential, so 0 is an essential singularity of sin⁡(1/z).

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-26Open item page →

1/sin(1/z) has a nonisolated singularity at 0

Statement refuted

Refuted claim: every singularity at a point of a complex function is automatically isolated.

The witness is

f(z)=1sin⁡(1/z)

at a=0. The function has poles at points tending to 0, so the singularity at 0 is not isolated.

Facts & Assumptions

Given: The function f(z)=1/sin⁡(1/z).

[L1]

The zeros of sine are exactly the integral multiples of π (The zero sets of sine and cosine and the least positive common period 2 pi).

Counterexample

technique · direct
1.1L1algebra

For every positive integer n, the point zn:=1/(nπ) satisfies sin⁡(1/zn)=sin⁡(nπ)=0 by [L1], so f has a pole at each zn.

2.1step 1.1algebra∎

The sequence (zn) tends to 0, so every punctured neighbourhood of 0 contains some pole of f. Hence no punctured neighbourhood of 0 is a region on which f is holomorphic, and the singularity at 0 is not isolated.

CounterexampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-26Open item page →

A Laurent series on a punctured disc can have infinitely many negative powers

Statement refuted

Refuted claim: every Laurent series on a punctured disc has only finitely many negative powers.

The witness is the Laurent expansion of e1/z on 0<∣z∣<1.

Facts & Assumptions

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

[L1]

Every holomorphic function on a punctured disc has a Laurent expansion there (Laurent expansion on an annulus).

[L2]

A finite nonzero principal part characterizes a pole (Characterizations of poles).

[L3]

The function e1/z has an essential singularity at 0 (e^{1/z} has an essential singularity at 0 and omits the value 0).

Counterexample

technique · direct
1.1L1

By [L1], the function e1/z has a Laurent expansion on 0<∣z∣<1.

2.1step 1.1L3

If that Laurent expansion had only finitely many negative powers, its principal part would be finite. It cannot be zero, because then the singularity would be removable and hence not essential. So the principal part would be finite and nonzero.

3.1step 2.1L2L3∎

By [L2], a finite nonzero principal part would make the singularity a pole, contradicting [L3]. Therefore the Laurent expansion of e1/z has infinitely many negative powers.

Sources