StoppedSelectedMass.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Summing the actual selected-prime rows over complementary products. The linear complementary mass is proved from roughness; it is not a Siegel--Walfisz hypothesis about the collected coefficient.

theorem OAI.CubicFirstMoment.stopped_selected_prime_mass_saving line 14