Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

sin⁡z−z has a zero of order three at the origin

Example

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

Facts & Assumptions

Given: The function h(z)=sin⁡z−z.

[L1]

The entire sine series is sin⁡z=∑n≥0(−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 ord⁡0(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 ord⁡0(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)=−cos⁡0=−1, confirming the same order and sign.

step 2.1L1L3L4∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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