OAI/NumberTheory/Ostmann/Preliminaries/SummandSizeProof.lean

The required summand-size theorem, without a published-input hypothesis

The proof uses the proved additive sieve and actual prime distribution. The finite fixed-shift sieve gives logarithmic growth, exponential sampling gives a concrete polynomial bootstrap, and the two-cutoff collision estimate gives the final square-root bounds. This supplies the exact consequence recorded from Elsholtz (2006), Theorem 1.9.