Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

Laurent series split into regular and principal parts

Statement

Let

f(z)=nZcn(za)n

be a convergent Laurent series on an annulus. Then:

  1. the regular part n0cn(za)n converges locally uniformly on every smaller disc za<R0<R, and on all of C when R=;
  2. the principal part m1cm(za)m (The principal part of a Laurent series) converges locally uniformly on every set za>ρ>r;
  3. on the original annulus, f is the sum of these two subseries.

Moreover, the regular and principal parts are uniquely determined by the Laurent coefficients.

Facts & Assumptions

Given: A Laurent expansion f(z)=nZcn(za)n on A(a;r,R).

[L1]

Laurent expansions exist on annuli and converge locally uniformly there (Laurent expansion on an annulus).

[L2]

Each Laurent coefficient is uniquely determined by the function on the annulus (Laurent coefficients are given by contour integrals and are unique).

Proof

technique · direct
1.1

Let 0<R0<R and choose σ with R0<σ<R; the coefficient formula gives cnMσ/σn for n0, where Mσ=maxζa=σf(ζ), so cn(za)nMσ(R0/σ)n for zaR0.

L2algebra
1.2

Let ρ>r and choose ρ0 with r<ρ0<ρ; the coefficient formula gives cmMρ0ρ0m for m1, where Mρ0=maxζa=ρ0f(ζ), so cm(za)mMρ0(ρ0/ρ)m for zaρ.

L2algebra
1.3

On the original annulus, [L1] gives that the Laurent series converges to f, and by definition that series is the sum of its nonnegative-power and negative-power subseries. So f=freg+fprin there.

givenL1
1.4

Uniqueness of the Laurent coefficients from [L2] makes both subseries unique term by term.

L2
2.1

The geometric majorant in step 1.1 converges, so the regular part converges uniformly on zaR0; since R0<R was arbitrary, the convergence is locally uniform on the disc of radius R, and when R= it is locally uniform on every bounded disc.

step 1.1
2.2

The geometric majorant in step 1.2 converges, so the principal part converges uniformly on zaρ; since ρ>r was arbitrary, the convergence is locally uniform on the exterior region za>r.

step 1.2
3.1

Steps 2.1, 2.2, 1.3, and 1.4 are exactly the claimed decomposition.

step 2.1step 2.2step 1.3step 1.4

Depends on

Used by

Dependency tree · two levels

13 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