Olson's growth dichotomy: $nA = \langle A\rangle$ or $|nA| \ge |A| + (n-1)\lfloor\tfrac{1}{2}(|A|+1)\rfloor$

Let $G$ be an abelian group, let $A \subseteq G$ be a finite set with $0 \in A$, and let $n \ge 1$. Write $nA = A + \cdots + A$ for the $n$-fold sumset and $\langle A \rangle$ for the subgroup generated by $A$. Because $0 \in A$ the iterates increase, $A \subseteq 2A \subseteq 3A \subseteq \cdots \subseteq \langle A \rangle$, and the theorem says that they increase quickly until they stop:

So each new summand buys at least $\lceil |A|/2 \rceil$ new elements, for as long as the whole generated subgroup has not yet been filled.

Proof idea (Olson). It suffices to prove the single-step bound $|nA| \ge |(n-1)A| + \tfrac12 |A|$ for $n > 1$ with $nA \ne \langle A \rangle$; the stated inequality then follows by iteration, using that $|nA|$ and $|(n-1)A|$ are integers to replace $\tfrac12|A|$ by $\lfloor\tfrac12(|A|+1)\rfloor$. For the step, $nA$ must be a proper subset of $(n+1)A$, since otherwise the iterates are eventually constant and $nA$ is a finite subgroup equal to $\langle A\rangle$. Pick $x \in (n+1)A \setminus nA$ and write $x = a_0 + y$ with $a_0 \in A$, $y \in nA$. Defining $k$ by $|nA| = |(n-1)A| + |A| - k$ and applying the Kemperman--Wehn theorem to the sumset $nA = (n-1)A + A$ at the element $y$, the set $A^* = \{a \in A : y - a \in (n-1)A\}$ has at least $k$ elements. Then $x - A^* \subseteq a_0 + (n-1)A \subseteq nA$, while $x - A^*$ is disjoint from $(n-1)A$ precisely because $x \notin nA$. Counting the two disjoint pieces inside $nA$ gives $|nA| \ge |(n-1)A| + k$, and combining this with the definition of $k$ eliminates $k$ and yields the step.

Sharpness. Olson's own remark: let $H$ be a finite subgroup and $x \notin H$ with $x + H = H + x$, and take $A = H \cup (x+H)$. For each $n$, either $nA = \langle A \rangle$ or $|nA| = (n+1)|H| = \tfrac12(n+1)|A|$, which is exactly $|A| + (n-1)\lfloor\tfrac12(|A|+1)\rfloor$ since $|A| = 2|H|$ is even. So neither the constant $\lfloor\tfrac12(|A|+1)\rfloor$ nor the dichotomy can be improved.

Formalization notes.

The iterated sumset. n • A is Mathlib's pointwise scalar iteration on Finset G, characterised by zero_nsmul : 0 • A = {0} and succ_nsmul : (n+1) • A = n • A + A. It is the sumset $A + \cdots + A$, not the image $\{n \cdot a : a \in A\}$.

The generated subgroup. $\langle A \rangle$ is AddSubgroup.closure (A : Set G). The alternative $nA = \langle A\rangle$ is stated as an equality of subsets of $G$, coercing the finite set n • A into Set G, because $\langle A \rangle$ carries no finiteness a priori — the content of that disjunct is exactly that the generated subgroup is finite and already exhausted by $n$ summands.

The floor. $\lfloor \tfrac12(|A|+1)\rfloor$ is (A.card + 1) / 2, natural-number division, matching the source's bracket notation $[\tfrac12(|A|+1)]$ ("$[m]$ denotes the greatest integer in $m$").

Truncated subtraction. n - 1 is $\mathbb{N}$-subtraction. The hypothesis hn : 0 < n is the source's "$n$ is a positive integer" and is genuinely needed: at $n = 0$ one has $0A = \{0\}$, so for any $A$ with $|A| \ge 2$ both alternatives fail.

Commutativity. Olson states Theorem 2.2 for an arbitrary group, and his proof is valid there. The card records the abelian case, [AddCommGroup G], which is what the rest of this mission consumes.