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

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

Analyticity of Holomorphic Functions; Liouville and Morera — 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 (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

sinzz has a zero of order three at the origin

Example

The entire function h(z)=sinzz has a zero of order 3 at 0.

Facts & Assumptions

Given: The function h(z)=sinzz.

[L1]

The entire sine series is sinz=n0(1)nz2n+1/(2n+1)! and has infinite radius of convergence (The exponential definitions of complex sine, cosine, hyperbolic sine, and hyperbolic cosine equal their entire power series).

[L2]

The order ord0(h) is the least natural index of a nonzero Taylor coefficient, and is + only when every coefficient is zero (The order of a zero of a holomorphic function).

[L3]

Finite order m is equivalent to a local factorization h(z)=zmg(z) with g holomorphic and g(0)0 (The order of a zero is the exponent in its local holomorphic factorization).

[L4]

Complex sine and cosine are entire and satisfy sin=cos and cos=sin (Complex sine, cosine, hyperbolic sine, and hyperbolic cosine are entire with their standard derivatives).

[L5]

The coefficients of a convergent complex power-series representation are uniquely the Taylor coefficients at its centre (The coefficients of a complex power series are its derivatives at the centre divided by the corresponding factorials).

Verification

technique · direct
1.1

Subtracting z from [L1] gives h(z)=z3/3!+z5/5!z7/7!+.

L1algebra
2.1

By [L5], the convergent representation in step 1.1 is the Taylor series of h at zero. Its coefficients in degrees 0, 1, and 2 vanish, while the coefficient in degree 3 is 1/3!0, so [L2] gives ord0(h)=3.

step 1.1L2L5
3.1

The factorization in [L3] therefore has h(z)=z3g(z) with g(0)=1/3!0; independently, [L4] and [L1] give h(0)=h(0)=0 and h(0)=cos0=1, confirming the same order and sign.

step 2.1L1L3L4
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-21Open item page →

Morera proves holomorphy of z01tzdt on Rez>1

Example

Let Ω={zC:Rez>1}. For t>0, use the principal power tz=exp(zlogt), and set 0z:=0 for zΩ. Then

F(z):=01tzdt

is holomorphic on Ω.

Facts & Assumptions

Given: The half-plane Ω={z:Rez>1} and the endpoint convention in the example.

[L1]

For a nonzero complex base t and exponent z, the principal power is tz=exp(zLogt); for positive real t, Logt=logt (Complex logarithms, the principal logarithm, and principal and multivalued complex powers, The natural logarithm as the inverse of the exponential function).

[L2]

The complex exponential is entire and has derivative equal to itself (The complex exponential is entire and its complex derivative is itself).

[L4]

The complex exponential agrees with the real exponential on the real axis (exp(z+w)=expzexpw, and the complex exponential extends the real exponential).

[L5]

The real exponential is strictly increasing (The exponential function is strictly increasing).

[L6]

The natural logarithm is continuous and strictly increasing on the positive reals, with log1=0 (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[L7]

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

[L8]

The composite of complex differentiable functions is complex differentiable (The chain rule for complex derivatives).

[L10]

A jointly continuous finite-interval integral of holomorphic parameter slices is holomorphic (A jointly continuous finite-interval parameter integral of holomorphic functions is holomorphic).

Verification

technique · direct
1.1

For t>0 define φ(t,z)=exp(zlogt) by [L1], and define φ(0,z)=0 as stated in the example.

givenL1
2.1

For fixed t>0, the map zzlogt is complex linear and [L2] with [L8] makes φ(t,) entire; for t=0 the slice is the constant zero function and is entire.

step 1.1L2L8
2.2

On (0,1]×Ω, [L3] and [L4] give φ(t,z)=exp((Rez)logt); [L6] gives logt0, so Rez>1 and [L5] yield φ(t,z)exp(logt)=t. Thus φ(t,z)0 uniformly for z near any fixed point of Ω as t0+; away from t=0, continuity follows from [L6], [L7], and the multiplication estimate from [L9], so φ is jointly continuous on [0,1]×Ω.

step 1.1L3L4L5L6L7L9algebra
3.1

Steps 2.1 and 2.2 satisfy [L10] on the finite interval [0,1], so F(z)=01φ(t,z)dt is holomorphic on Ω.

step 2.1step 2.2L10
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-21Open item page →

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
CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-21Open item page →

zn tends locally uniformly to zero on the unit disc but not uniformly on the closed disc

Statement refuted

Refuted claim: Local uniform convergence on the open unit disc forces uniform convergence on the closed unit disc.

For fn(z)=zn, the sequence (fn) converges locally uniformly to 0 on D={z:z<1}, but it does not converge to 0 uniformly, or even pointwise, on D.

Facts & Assumptions

Given: The functions fn(z)=zn and the local-uniform convention of Locally uniform convergence on an open subset of the complex plane is compact convergence.

[L1]

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).

[L3]

Uniform convergence to zero requires that for every ε>0, all sufficiently late functions have modulus below ε at every point of the domain (Uniform convergence and the uniformly Cauchy condition for complex-valued functions, with the componentwise dictionary).

[L4]

Complex modulus satisfies zwzw, so zz is continuous (Conjugation is an involutive real-field automorphism, zz=z2, and modulus is definite, multiplicative, and subadditive).

Counterexample

technique · direct
1.1

Let KD be compact. If K=, uniform convergence on K is vacuous. Otherwise [L4] and [L1] give q=maxzKz, and q<1 because the maximum is attained at a point of KD; then fn(z)=znqn0 by [L2], uniformly for zK.

L1L2L4
1.2

At the boundary point z=1, one has fn(1)=1 for every natural n, including n=0, so the sequence does not converge pointwise to zero there and fails the uniform condition [L3] on D.

L3algebra
2.1

Step 1.1 proves local uniform convergence on the open disc, while step 1.2 proves failure on its closure, so the claimed implication is false.

step 1.1step 1.2
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Morera's theorem fails without continuity

Statement refuted

Refuted claim: A function on an open subset of C whose integral around every contained triangle is zero must be holomorphic, even when continuity is not assumed.

In the edgewise Riemann sense, the function

f(z):={1,z=0,0,z0

has zero integral around every complex triangle, but is not holomorphic.

Facts & Assumptions

Given: The displayed function f:CC and an arbitrary ordered complex triangle.

[L1]

If the velocity-weighted pullback of a function along each affine triangle edge is Riemann integrable, its edgewise triangle integral is the sum of those edge integrals (The edgewise Riemann integral around a complex triangle for an integrable pullback).

[L2]

Changing a real Riemann-integrable function at finitely many points preserves integrability and its integral (Changing an integrable function at finitely many points changes neither its integrability nor its integral).

[L3]

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

[L4]

Morera's theorem assumes continuity in addition to zero integrals around every contained filled triangle (Morera's theorem: vanishing triangle integrals characterize holomorphy among continuous functions).

Counterexample

technique · direct
1.1

Fix an arbitrary triangle and read its boundary integral in the edgewise sense of [L1] for the point-supported function f.

givenL1
1.2

The function is discontinuous at 0, since every punctured neighbourhood contains points where its value is 0 while f(0)=1; by [L3], it is not complex differentiable, and hence not holomorphic, at 0.

givenL3
2.1

On a nonconstant affine edge, the edge map is injective and therefore meets 0 at most once, so each real component of its velocity-weighted pullback differs from zero at at most one parameter and [L2] makes its integral zero; on a constant edge the velocity is zero, so its pullback integral is also zero. Hence [L1] gives zero around every triangle, including repeated or collinear vertices.

step 1.1L1L2
3.1

Steps 2.1 and 1.2 exhibit vanishing edgewise triangle integrals without holomorphy, so removing the continuity hypothesis from [L4] makes the implication false.

step 2.1step 1.2L4
False statementConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-21Open item page →

FALSE: every smooth map between open subsets of the plane is real analytic

Statement

False claim: Every smooth map between open subsets of R2 is real analytic.

Facts & Assumptions

Given: The function ϕ:RR and planar map F:R2R2 defined by

ϕ(x):={exp(1/x2),x0,0,x=0,F(x,y):=(ϕ(x),0).

[L1]

The real exponential is C and every derivative of it is the exponential itself (The exponential function is smooth and (exp)=exp).

[L4]

For every natural m and real a>0, xm/exp(ax)0 as x+ (The exponential dominates every fixed nonnegative integer power at +).

[L5]

A planar real function is Ck when every coordinate-derivative word of length at most k, including the word of length zero, exists and is continuous (Ck maps and multi-index derivative notation in Euclidean space).

[L6]

A smooth map G=(u,v) is real analytic when, near every point, both components equal their total-degree Taylor series (Real-analytic maps between open subsets of the coordinate plane).

[L7]

The real exponential is positive everywhere and satisfies exp(x)=1/exp(x) (The exponential is positive and satisfies exp(x)=1/exp(x)).

Refutation

technique · direct
1.1

For every natural m, repeated use of [L1], [L2], and [L3] gives a real polynomial Pm such that ϕ(m)(x)=Pm(1/x)exp(1/x2) for x0: take P0=1, and differentiation replaces Pm(y) by the polynomial y2Pm(y)+2y3Pm(y).

L1L2L3
2.1

As x0, every expression P(1/x)exp(1/x2) and its quotient by x tends to 0: with y=1/x+, polynomial growth is bounded by a natural power of y, which for y1 is bounded by a natural power of y2, and [L4] applied to u=y2 makes that power times exp(u) tend to zero.

step 1.1L4
3.1

Inductively set every derivative value ϕ(m)(0)=0: step 2.1 makes ϕ(m) continuous at 0 and makes its difference quotient there tend to 0, so the next derivative exists and has value 0. Thus ϕ is smooth, and [L5] makes F(x,y)=(ϕ(x),0) smooth with every mixed derivative at (0,0) equal to 0.

step 2.1L5
4.1

By step 3.1, the total-degree Taylor series of F at (0,0) is the zero map, but [L7] gives F(x,0)=(exp(1/x2),0)(0,0) for every x0; such points occur in every neighbourhood of the origin, so the equality required by [L6] fails there.

step 3.1L6L7
5.1

The map F is smooth by step 3.1 and not real analytic by step 4.1, so it refutes the false claim.

step 3.1step 4.1
False statementConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

FALSE: an entire function bounded on the real axis is constant

Statement

False claim: If an entire function is bounded on the real axis, then it is constant.

Facts & Assumptions

Given: The complex sine function.

[L1]
[L2]

Complex sine restricts to the published real sine function on the real axis (The exponential formulas, real restrictions, and trigonometric-hyperbolic dictionary over C).

[L3]

For every real x, sinx1 (Parity and the Pythagorean identity for sine and cosine).

[L4]

Complex sine and cosine are entire and satisfy sin=cos and cos=sin (Complex sine, cosine, hyperbolic sine, and hyperbolic cosine are entire with their standard derivatives).

Refutation

technique · direct
1.1

By [L1] and [L4], complex sine is entire; by [L2] and [L3], its restriction to the real axis satisfies sinx1 for every real x.

L1L2L3L4
1.2

By [L4], the derivative of sine is cosine, and the series in [L1] gives cos0=1, so sine has a nonzero derivative and is not constant.

L1L4algebra
2.1

Steps 1.1 and 1.2 give an entire function bounded on the real axis but not constant, refuting the claim; this does not contradict Liouville's theorem: every bounded entire function is constant, whose hypothesis is boundedness on the whole complex plane.

step 1.1step 1.2
False statementConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

FALSE: every entire function with an antiderivative is a polynomial

Statement

False claim: Every entire function that has an entire antiderivative is a polynomial.

Facts & Assumptions

Given: The complex exponential function.

[L1]

The complex exponential is entire and satisfies exp=exp on C (The complex exponential is entire and its complex derivative is itself).

[L2]

For all complex z,w, exp(z+w)=expzexpw, and the complex exponential agrees with the real exponential on the real axis (exp(z+w)=expzexpw, and the complex exponential extends the real exponential).

[L3]

Every nonconstant complex polynomial has a complex root (Fundamental theorem of algebra: every nonconstant complex polynomial has a complex root).

[L4]

The normalized real exponential satisfies exp0=1 and has derivative 1 at 0 (Regular normalized multiplicative Cauchy equations characterize the exponential).

Refutation

technique · direct
1.1

By [L1], the complex exponential is entire and is its own entire antiderivative.

L1
1.2

By [L2] and [L4], expzexp(z)=exp0=1, so the exponential never vanishes; [L1] then makes its derivative nonzero everywhere, and it is nonconstant.

L1L2L4algebra
2.1

If the complex exponential were a nonconstant polynomial, [L3] would give it a complex zero, contradicting step 1.2.

step 1.2L3
3.1

It is not a constant polynomial because its derivative is nonzero by step 1.2, and step 2.1 excludes every nonconstant polynomial; together with step 1.1, the exponential is an entire nonpolynomial function with an entire antiderivative, refuting the claim.

step 1.1step 1.2step 2.1

Sources