ScalarBinaryGrowth.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Iterating the actual binary switching construction. The final points remain in one fixed-fold sumset, while their number grows at every level.