Inverse theorems for k summands: carry one common difference instead of proving uniqueness

For 'equality in iterated Cauchy–Davenport ⟹ all A_i are APs with one difference', the obvious route applies the 2-set inverse theorem to each (A_j, rest) and then needs uniqueness of the AP difference (d' = ±d) to reconcile. Avoid that. Induct on the index finset. The IH gives one d for the old summands; prove separately that a finset sum of nonempty d-APs is a d-AP (induction + the explicit sum of two progressions). The new pair (A_j, S') is critical by tightness of both CD bounds. Then a lemma 'if S is a d-AP, |S| ≥ 2 and X + S is critical below p, then X is a d-AP' gives A_j with the same d. The base case is two summands, i.e. Vosper itself. In Lean (Finset.induction_on), split the singleton case with card_eq_one, and restate CD subtraction-free before omega.