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

Uniform convergence on the closed unit disc does not give a holomorphic extension to a larger disc

Statement refuted

Refuted claim: If a complex power series converges uniformly on a closed disc, its sum extends holomorphically to some larger centred disc.

The series

F(z):=n1znn2

converges uniformly on z1, but its sum on z<1 has no holomorphic extension to any disc centred at 0 with radius greater than 1.

Facts & Assumptions

Given: The complex power series defining F, with its partial sums and convergence interpreted as in Complex series, absolute convergence, complex power series, and radius of convergence.

[L1]

If fn(x)Mn and the real series Mn converges, then the complex function series fn converges absolutely pointwise and uniformly (Weierstrass M-test for complex-valued function series).

[L2]

The series n11/n2 converges, while the harmonic series n11/n diverges (For rational p>0, 1/kp converges iff p>1).

[L3]

Inside the radius of convergence, a complex power series may be differentiated term by term: (n0cnzn)=n1ncnzn1 (Inside its disc of convergence a complex power series is holomorphic and may be differentiated term by term).

[L4]

A continuous real-valued function on a nonempty compact metric space is bounded and attains a maximum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[L5]

A complex differentiable function is continuous (Complex differentiability at a point implies continuity there).

[L8]

Complex modulus is multiplicative and satisfies the triangle inequality, hence uvuv (Conjugation is an involutive real-field automorphism, zz=z2, and modulus is definite, multiplicative, and subadditive).

[L9]

Every holomorphic function has complex derivatives of every order locally (All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle).

Counterexample

technique · contradiction
1.1

On z1, one has zn/n21/n2, so [L1] and the convergent series in [L2] give absolute pointwise and uniform convergence of the displayed series.

L1L2
1.2

For real 0<r<1, [L3] gives F(r)=n1rn1/n.

L3
1.3

Suppose, for contradiction, that a function G holomorphic on D(0,S) for some S>1 agrees with F on z<1. By [L9], G is holomorphic near [0,1], hence continuous by [L5]; [L8] makes G continuous, [L7] makes [0,1] compact, and [L4] bounds G there.

L4L5L7L8L9assume-contra
2.1

Given B>0, divergence in [L2] supplies N2 with n=1N1/n>2B; by [L6] and [L5], the finitely many monomials rn1 are continuous at r=1, so choose 0<r<1 with rn1>1/2 for every 1nN, and step 1.2 then gives F(r)>12n=1N1/n>B.

step 1.2L2L5L6choose
3.1

Step 2.1 makes F(r)=G(r) exceed every proposed bound for points 0<r<1, contradicting step 1.3; no such extension exists, and the refuted claim is false.

step 2.1step 1.3discharge-contradiction

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

80 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