SmallBCoreHybrid.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform core bounds with an explicit logarithmic cutoff parameter. Ordinary character duality handles moderately small conductors and the cubic sieve handles the remaining ones.

theorem OAI.CubicFirstMoment.smallB_core_hybrid_sieve line 13