The accumulated deficit in Olson's Theorem 3.1 is below $s^2/72$

This is the one analytic estimate that Olson's Theorem 3.1 reduces to once its bookkeeping is separated out, and it contains no group theory.

Olson's recursion runs $y_2=4$ and $y_{t+1}=y_t+\min\{\tfrac{y_t+1}{2},\tfrac{s-t+2}{4}\}$. The first branch wins exactly on an initial segment of steps $2\le t\le u$, and on that segment $y_t+1=5(3/2)^{t-2}$ exactly, so the shortfall against the second branch at step $t$ is

The hypothesis $10(3/2)^{u-2}<s-u+2$ says the first branch is still winning at step $u$, which is what makes every $d_t$ for $2\le t\le u$ nonnegative. The claim is that the total shortfall stays below $s^2/72$ — the quantity Olson calls $\Delta(s)$, and the reason his constant reads $c=\tfrac18-O(\log s/s)$. Since $\tfrac18-\tfrac1{72}=\tfrac19$, this estimate is exactly what produces the constant $\tfrac19$ of Theorem 3.2.

Why the easy route fails. One would like to bound the sum by (number of terms) $\times$ (largest term) and then use $u<s/18$. That does not work: $u<s/18$ is false for every $11\le s\lesssim 190$ — at $s=44$ the phase runs to $u=5$ while $s/18\approx 2.44$ — and this is precisely the range where the inequality is tightest. Counterexample testing over all admissible pairs with $s\le 1200$ gives a worst ratio of $0.825$ at $(s,u)=(44,5)$, so only about $17\%$ of slack is available and the geometric term must be kept. Olson himself splits into $u\ge 10$, where $10(3/2)^{u-3}+u-3<s$ yields $s>18(u-2)$, and $3\le u\le 9$ checked directly.

Formalization Note. Fully arithmetic: a finite sum of reals, no algebraic structure. The exponents $t-2$ and $u-2$ are natural-number subtractions, harmless because $t\ge 2$ throughout Finset.Icc 2 u and $u\ge 2$ by hypothesis. The statement is asserted for every $u$ satisfying the phase hypothesis, not only the maximal one; since all summands are then nonnegative, the partial sums are monotone and the maximal $u$ is the worst case.