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

The exponential definitions of complex sine, cosine, hyperbolic sine, and hyperbolic cosine equal their entire power series

Statement

For every zC, sinz=n0(1)nz2n+1(2n+1)!,cosz=n0(1)nz2n(2n)!, sinhz=n0z2n+1(2n+1)!,coshz=n0z2n(2n)!. All four series have infinite radius.

Facts & Assumptions

Given: A complex number z.

[L1]

The complex exponential is defined by the series expz=n0zn/n!, the cited Definition recording that convergence for every zC is discharged elsewhere (The complex exponential by its power series).

[L2]

Sine, cosine, hyperbolic sine, and hyperbolic cosine are the symmetric and antisymmetric exponential combinations displayed in their definition (Complex sine, cosine, hyperbolic sine, and hyperbolic cosine from the complex exponential).

[L3]

Every absolutely convergent complex series may be rearranged without changing its sum (Every absolutely convergent complex series converges, and rearrangements preserve its sum).

[L4]

If L=lim supkck+11/(k+1), Cauchy–Hadamard gives radius + when L=0 (Cauchy-Hadamard for complex power series, including zero and infinite radius).

[L5]

For every zC the series zn/n! converges absolutely (The complex exponential series converges absolutely for every complex argument).

Proof

technique · direct
1.1

Substitute the series [L1] at z,z,iz,iz into [L2]. Absolute convergence, which [L5] supplies for every complex argument, allows [L3] to separate the even and odd indices.

L1L2L3L5
2.1

The identities i2n=(1)n and i2n+1=i(1)n simplify those even and odd parts to the four displayed series.

step 1.1algebra
3.1

Their factorial coefficients have root limsup 0: for n2 the factorial satisfies n!(n/2)n/2, since at least n/2 of the factors 1,,n are at least n/2, so (1/n!)1/n(2/n)n/2/n0. Hence [L4] gives infinite radius. The constant terms are retained in the even series and absent from the odd series.

step 2.1L4

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 100 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources