Olson's Theorem 3.1: quantitative arrangement bound $|\Sigma(a_1,\dots,a_t)| > 4+\frac18[(s-2)(s+3)-(s-t)(s-t+5)]-\frac{s^2}{72}$

Let $S$ be a set of $s\ge3$ distinct non-zero elements of an abelian group $G$ with $\langle S\rangle=G$, and for a sequence $a_1,\dots,a_t$ write

$$\Sigma(a_1,\dots,a_t)=\{0,a_1\}+\{0,a_2\}+\cdots+\{0,a_t\}.$$

Olson's Theorem 3.1 asserts that there is an arrangement $a_1,\dots,a_s$ of the elements of $S$ and an index $2\le q\le s$ such that either $\Sigma(a_1,\dots,a_{s-1})=G$, or both of the following hold.

(i) For all $2\le t\le q$,

$$|\Sigma(a_1,\dots,a_t)|\ \ge\ 4+\tfrac18\bigl[(s-2)(s+3)-(s-t)(s-t+5)\bigr]-\Delta(s),$$

where $O(s\log s)=\Delta(s)<s^2/72$.

(ii) If $q<s$ then $H=\langle a_{q+1},\dots,a_s\rangle$ is a finite proper subgroup of $G$ and $|H|<2\min\{|\Sigma|,|\bar\Sigma|\}$, where $\Sigma=\Sigma(a_1,\dots,a_q)$.

What $\Delta(s)$ is, and why the card does not carry it. $\Delta(s)$ is not given in closed form in the paper; it is defined inside the proof (equations (10)–(15)). Define $y_2=4$ and, for $2<t\le s$,

$$y_t=y_{t-1}+\min\Bigl\{\tfrac12(y_{t-1}+1),\ \tfrac14(s-t+3)\Bigr\}. \tag{10}$$

For $s\le10$ the first branch never wins and $\Delta(s)=0$. For $s\ge11$ let $u=u(s)$ be the largest integer with $3\le u<s-1$ and $\tfrac12(y_{u-1}+1)<\tfrac14(s-u+3)$; then $y_t=5(3/2)^{t-2}-1$ for $2\le t\le u$, and

$$\Delta(s)=\sum_{j=3}^{u}\Bigl[\tfrac14(s-j+3)-\tfrac12(y_{j-1}+1)\Bigr]=\tfrac18\bigl\{2s(u-2)+u(5-u)+26-8y_u\bigr\}. \tag{15}$$

Olson then shows $\Delta(s)<s^2/72$ for every $s$, which is precisely the slack that turns the constant $\tfrac18$ of (i) into the constant $\tfrac19$ of Theorem 3.2: $\tfrac18-\tfrac1{72}=\tfrac19$.

Since $\Delta$ is used downstream only through the bound $\Delta(s)<s^2/72$, this card states (i) with $s^2/72$ in place of $\Delta(s)$ and with a strict inequality:

$$|\Sigma(a_1,\dots,a_t)|\ >\ 4+\tfrac18\bigl[(s-2)(s+3)-(s-t)(s-t+5)\bigr]-\frac{s^2}{72}.$$

This is implied by Olson's (i) together with $\Delta(s)<s^2/72$, so the card is a consequence of the source's statement and needs no new definition. It is still strong enough for Theorem 3.2: taking $t=s$ it gives $|\Sigma|>\tfrac{13}4+\tfrac{s}{8}+\tfrac{s^2}{9}$, and in general it yields the paper's equation (16), $|\Sigma(a_1,\dots,a_t)|>3+cs^2-\tfrac18(s-t)(s-t+5)$ with $c=\tfrac19$, which is exactly what the induction in Theorem 3.2 consumes.

Formalisation notes. In an abelian group $\Sigma(a_1,\dots,a_t)$ depends only on the set $\{a_1,\dots,a_t\}$, so an arrangement is recorded by its chain of prefixes $A_t=\{a_1,\dots,a_t\}$: a function A : ℕ → Finset G with A 0 = ∅, A t ⊆ A (t+1), (A t).card = t for t ≤ s, and A s = S. A chain of this shape is the same data as an arrangement of $S$. Then $\Sigma(a_1,\dots,a_t)$ is (A t).powerset.image (fun U => ∑ x ∈ U, x), the notation used throughout this mission, and $\langle a_{q+1},\dots,a_s\rangle$ is the subgroup generated by $S\setminus A_q$. The alternative $\Sigma(a_1,\dots,a_{s-1})=G$ is written as "every $g:G$ lies in that image", which is the correct reading in an infinite group as well. The comparison $|H|<2\min\{|\Sigma|,|\bar\Sigma|\}$ is made in ℕ∞, since $\bar\Sigma$ can be infinite while $\Sigma$ is always finite.

Olson states the theorem for an arbitrary group; this card is the abelian case, which is the one this mission consumes.

import Definitions.Def_Erdos131_NonDividing
import Mathlib.Tactic
open Erdos131

theorem Erdos131.olson_thm3_1 {G : Type*} [AddCommGroup G] [DecidableEq G]
    (S : Finset G) (s : ℕ) (hcard : S.card = s) (hs : 3 ≤ s)
    (h0 : (0 : G) ∉ S) (hgen : AddSubgroup.closure (S : Set G) = ⊤) :
    ∃ A : ℕ → Finset G,
      A 0 = ∅ ∧ A s = S ∧ (∀ t, A t ⊆ A (t + 1)) ∧ (∀ t ≤ s, (A t).card = t) ∧
      ∃ q : ℕ, 2 ≤ q ∧ q ≤ s ∧
        ((∀ g : G, g ∈ (A (s - 1)).powerset.image fun U => ∑ x ∈ U, x) ∨
          ((∀ t, 2 ≤ t → t ≤ q →
              4 + (((s : ℝ) - 2) * ((s : ℝ) + 3)
                    - ((s : ℝ) - (t : ℝ)) * ((s : ℝ) - (t : ℝ) + 5)) / 8
                - (s : ℝ) ^ 2 / 72
              < (((A t).powerset.image fun U => ∑ x ∈ U, x).card : ℝ)) ∧
            (q < s →
              (AddSubgroup.closure ((S \ A q : Finset G) : Set G) : Set G).Finite ∧
              AddSubgroup.closure ((S \ A q : Finset G) : Set G) ≠ ⊤ ∧
              ((AddSubgroup.closure ((S \ A q : Finset G) : Set G) : Set G).encard <
                2 * min ((((A q).powerset.image fun U => ∑ x ∈ U, x).card : ℕ) : ℕ∞)
                  ((((A q).powerset.image fun U => ∑ x ∈ U, x : Finset G) : Set G)ᶜ.encard))))) := by sorry