Nathanson observed, and Senger proved, that for four-element integer sets A the most frequent sizes of the iterated sumset hA are separated by triangular numbers. The task is to extend this pattern to k-element subsets of {1,...,q} for every k≥3.

Collisions in hA are encoded as primitive integer coefficient vectors d with coordinate sum zero, weight at most h, and d·A=0. The number of sets orthogonal to one such vector, or to two of them, is bounded by lattice-point counts. Sets orthogonal to exactly one vector of weight s are shown to have |hA| = M_{h,k} − M_{h−s,k}. The full development is formalized in Lean 4 with Mathlib, partly by hand and partly generated by the Aristotle prover.

For fixed k≥3 and h fixed or growing slower than q^{1/(2k-1)}, almost every k-subset of [q] is a B_h-set. Almost every exception has one of h−1 explicit smaller sumset sizes, and the gaps between consecutive sizes are consecutive (k−2)-dimensional simplex numbers. All proofs are checked by the Lean kernel, except one finite computation that relies on native_decide.