Olson's Theorem 3.1 bookkeeping: the bound is the running sum of Lemma 3.1's credit, minus an accumulated deficit

Olson's Theorem 3.1 bounds $|\Sigma(a_1,\ldots,a_t)|$ below by

less an error term $\Delta(s)$. The proof runs the recursion of his equation (10): $y_2=4$ and

the two branches being the two alternatives supplied by Lemma 3.1. This theorem is the exact bookkeeping of that recursion. Writing $d_t$ for the shortfall at step $t$ — the amount by which the minimum falls below its second branch — it states two things:

1. Every shortfall is nonnegative: $d_t\ge 0$ for all $t$.
2. The recursion telescopes exactly: for $2\le t\le s$,

So $f$ is precisely the closed form of the second branch run alone: $f(2)=4$ and $f(t+1)-f(t)=\tfrac14(s-t+2)$, an identity the proof verifies directly. Every step where the first branch wins costs exactly $d_t$, and the total cost is what Olson calls $\Delta(s)$.

What this isolates. Theorem 3.1 reduces to a single analytic estimate on the accumulated shortfall, namely $\sum_j d_j<s^2/72$; no part of the group theory remains in it. The first branch wins exactly on an initial segment $3\le t\le u$ of steps, on which $y_t=5(3/2)^{t-2}-1$ grows geometrically, so $u=O(\log s)$ and the total shortfall is $O(s\log s)$ — this is the source of Olson's $c=\tfrac18-O(\log s/s)$, and $\tfrac18-\tfrac1{72}=\tfrac19$ is how the constant $\tfrac19$ of Theorem 3.2 arises.

Formalization Note. The recursion is taken as a hypothesis on given functions $y,d$ rather than as a new definition, so the statement needs no addition to the mission's definition bundle. Indices are shifted by one against the source so that the step hypothesis reads forward, from $t$ to $t+1$. The sum is over Finset.Ico 2 t, which is empty at $t=2$ and gives the base case.