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

Cauchy's inequalities bound the Taylor coefficients by the circle supremum

Statement

Let f be holomorphic on D(a,R), let 0<r<R, and suppose M≥0 satisfies ∣f(ζ)∣≤M whenever ∣ζ−a∣=r. If cn=f(n)(a)/n! is the nth coefficient of the Taylor series of f at a, then

∣cn∣≤Mrn(n∈N).

If ∣f(ζ)∣≤M on ∣ζ−a∣=r, then the nth Taylor coefficient cn satisfies ∣cn∣≤M/rn.

Facts & Assumptions

Given: A holomorphic function f on D(a,R), a radius 0<r<R, a bound M≥0 on the radius-r circle, and a natural n.

[L1]

The Taylor series of f at a is ∑n≥0f(n)(a)(z−a)n/n! (The Taylor series of a holomorphic function at a point).

[L2]

Under the hypotheses above, ∣f(n)(a)∣≤n!M/rn for every natural n (Cauchy's inequalities bound every derivative by a boundary bound on a compactly contained circle).

Proof

technique · direct
1.1

By [L1], cn=f(n)(a)/n!, while [L2] gives ∣f(n)(a)∣≤n!M/rn.

L1L2
2.1

Since n! is positive and r>0, division in step 1.1 is legitimate and yields ∣cn∣≤M/rn; for n=0 this is ∣f(a)∣≤M, and the same calculation permits M=0.

step 1.1algebra∎

Depends on

Used by

Dependency tree · two levels

7 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