Term Bounds Do Not Bound Growing Family Sums

Abstract

Growing finite families can keep a nonzero sum despite vanishing term bounds.

Theorem 1.1 (Small terms do not force a growing family sum to vanish).

$$\begin{gathered} \forall \gamma \in \mathbb{N},0<\gamma \Rightarrow \\ \exists \epsilon :\mathbb{N}\to \mathbb{R},n:\mathbb{N}\to \mathbb{N},A:\forall m,\mathrm{Fin}\left(n_m\right)\to \mathbb{R}, \\ \underset{m\to \infty }{\lim }{\epsilon }_m=0\wedge \forall m,0<{\epsilon }_m\wedge \\ \forall m,i\in \mathrm{Fin}\left(n_m\right),|A_{m,i}|\le {\epsilon }_m^{\gamma }\wedge \\ \forall m,\sum _{i\in \mathrm{Fin}\left(n_m\right)}|A_{m,i}|=1\wedge \\ \neg (\underset{m\to \infty }{\lim }\sum _{i\in \mathrm{Fin}\left(n_m\right)}|A_{m,i}|=0). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/AnalyticClosure/FamilySums/TermBoundDoesNotBoundFamilySum.term_bound_does_not_bound_family_sum (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every given positive natural exponent gamma, the witness takes epsilon_m equal to 1/(m+1), a family of (m+1)^gamma members, and identical amplitudes epsilon_m^gamma. The scale is positive and tends to zero, and every amplitude meets the bound with equality.

Summing the (m+1)^gamma absolute amplitudes gives exactly one for every m. The family sums are therefore bounded away from zero and cannot converge to zero, even though the individual bound vanishes.

A separate Lean example fixes the family size at one and verifies that its sum does converge to zero. This distinguishes the growth obstruction from a universal failure of termwise decay.

The source’s six controls, covering analytic gain, object counts, cancellation grouping, cut termination, truncation remainders, and time-block accumulation, are a research checklist rather than mathematical assertions and are not encoded as propositions.

References

• Truth anchor: D5/S3/AnalyticClosure/FamilySums/TermBoundDoesNotBoundFamilySum.term_bound_does_not_bound_family_sum