OAI/NumberTheory/TotientAsymptotic/PPTNormalWitnessCount.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The nonnormal-target discard in the PPT construction, at the existing dyadic counting-envelope scale. The finite singleton-fiber argument allows the unconditional exceptional-totient estimate to count the original candidate integers without any multiplicity loss.

  1. theorem OAI.TotientAsymptotic.ppt_nonnormal_witness_count_bound line 17