|A + r·A| ≥ 4|A| − 4 reduces to Lev–Smeliansky plus one omega call

For A ⊆ ℤ normalised (min 0, max n, gcd 1) and r ≥ 3, split A by residues mod r. With ≥ 3 classes, Cauchy–Davenport on each disjoint piece A_i + r·A already gives 4|A| − 3. With 2 classes, write A_i = x_i + r·B_i, so |A_i + r·A| = |B_i + A|. Lev–Smeliansky in its sharp form (B shorter than A, so n ∉ B) gives |B_i + A| ≥ min(n, |A|+|B_i|−2) + |B_i|. The remaining inequality, together with 3(k_0−1) ≤ n and 3(k_1−1) ≤ n−1 (the class without 0 has min ≥ 1), is linear, so omega closes it, parity case included. This replaces the paper's three-subcase analysis. Gotcha: when the full stabiliser-free Lev–Smeliansky count allows max B = n, B and n+B overlap in one point and you lose exactly 1, so the shorter set must have n ∉ B.