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.
Formal factorial series with zero convergence radius — Counterexample
1 · Prerequisites
None. This page is self-contained.
2 · Summary
The counterexample is a valid formal coefficient sequence but diverges at every nonzero complex , so its numerical radius of convergence is zero. This shows why formal coefficient manipulations alone do not imply an analytic function or a truncation error bound. It makes no claim about convergence or summability of any particular QFT expansion.
3 · Logical flowchart
4 · Definitions, postulates, theorems and proofs
None yet.
5 · Examples, experiments and counterexamples
Every formal coefficient exists while convergence radius vanishes
Statement refuted
Define to be the set of coefficient sequences , written , with coefficientwise equality and addition and Cauchy multiplication: the coefficient of in a product is , a finite sum. Formal membership makes no numerical convergence assertion. For numerical evaluation use for every , including ; numerical convergence means convergence of the partial sums in . In the extended nonnegative reals , the numerical radius of a coefficient sequence is
where the supremum is taken in the extended order, so when the set is unbounded. The claim to refute is that every element of has .
For , define , with the empty product ; thus . View these integer products as coefficients in through the canonical embedding .
Facts & Assumptions
Given: A formal variable and the coefficient sequence for all .
The formal operations and coefficientwise equality are as defined in the Statement; the coefficient sequence itself does not assert convergence after numerical evaluation.
Each is a positive integer, hence a nonzero coefficient in ; positivity follows by induction from and with .
Counterexample
Each is a finite complex number by [F1], so the sequence defines an element of by [A1], irrespective of numerical convergence.
Fix any and put . By [F1], , so for every ; the factorial recurrence in the Statement therefore gives , which is greater than for all sufficiently large . Hence eventually grows by a factor greater than at every step, so does not tend to zero.
If the numerical series converged, its partial sums would converge, so as ; step 1.2 rules this out for every nonzero . At , [F1] and the convention leave only the constant term, so the series equals . Thus the series converges at no nonzero . For every real , the point lies in and gives divergence, so no positive satisfies the defining property of the radius; satisfies it vacuously. Therefore the defining set is exactly , its supremum in is , and the claimed positive radius fails.
Remarks
This example separates coefficientwise formal algebra from numerical convergence. It proves no convergence, summability, or divergence claim for any particular QFT perturbation series. A truncation error requires a separate estimate for a specified analytic model; formal coefficient identities alone do not provide one.