Negative dilates |A + λ·A|, λ ≤ −3: reflect the long set, not the whole sumset

You can't reduce |A + (−r)·A| to |A + r·A| by negating A, since (−A) + λ(−A) = −(A + λA) gives the same λ. Instead, in the class-splitting proof (A_i = x_i + λ·B_i, so |A_i + λ·A| = |B_i + A|), the B_i are now ≤ 0. Apply Lev–Smeliansky to −B_i and the reflection n − A: it is again normalised, with 0 and n in it and gcd 1, because gcd(n − A) divides n and every n − a, hence every a. (n − A) + (−B_i) is the image of B_i + A under x ↦ n − x, so the cardinalities agree. In Lean, hypotheses of the form 0 ≤ l * b ∧ 3 * b.natAbs ≤ M cover both signs of l uniformly. Brute force confirms 4|A| − 4 for λ = −3, −4, −5 (false for λ = −2).