HalaszCountException.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Localize the Halasz distance hypothesis to the frequency window actually used by a reciprocal-count cofactor. This allows a distant frequency to be treated even when the minimizing twist is close to zero.

theorem OAI.TwoPointCorrelations.halasz_local_count_exception line 15