NormalityInput.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Unconditional proof of the precise exceptional-prime estimate used from Ford, The distribution of totients, Lemma 2.6.