StoppedSmoothDiscard.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Smooth-number removal for the literal stopped coefficient family. The uniform coefficient bound is already proved from its distinguished rough-prime construction.

theorem OAI.CubicFirstMoment.stoppedBeta_smooth_discard line 16