PublishedSummandBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Published counting bounds for the summands

Christian Elsholtz, Additive decomposability of multiplicatively defined sets, Functiones et Approximatio Commentarii Mathematici 35 (2006), 61–77, Theorem 1.9, printed p. 63. DOI: 10.7169/facm/1229442617. https://www.math.tugraz.at/~elsholtz/WWW/papers/papers22wirsing04.pdf

We record just its square-root counting consequence for a hypothetical asymptotic decomposition, in the nonnegative-integer convention of the target manuscript (Section 2, Lemma size). This is an explicit conditional input; no instance is postulated globally. The tail truncation is proved separately.

def OAI.Ostmann.PublishedSummandSizeBound line 23
Source documentation
The only counting-function estimates needed from Elsholtz's Theorem 1.9.
```
def PublishedSummandSizeBound : Prop :=
…
```