LocalSuffixPruning.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Assemble the proved exceptional classes before the surviving Ford comparison count. The remaining premise is a finite reciprocal estimate for the explicitly defined regular witness class.

theorem OAI.TotientAsymptotic.local_suffix_count_of_regular_mass line 14