Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

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]

The complex sine is defined from the complex exponential, and sin⁡(iu)=isinh⁡(u) for real u (Complex sine, cosine, hyperbolic sine, and hyperbolic cosine from the complex exponential, The exponential formulas, real restrictions, and trigonometric-hyperbolic dictionary over C).

[L2]

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

Counterexample

technique · direct
1.1

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

givenalgebra
1.2

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.

L1algebra
2.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.

step 1.1
3.1

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

step 1.2step 2.1L2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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