OAI/NumberTheory/TotientAsymptotic/FixedBandExceptions.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Fixed terminal truncation first, then a growing retained-coordinate cutoff: this order makes the actual model-band exception count negligible.

  1. theorem OAI.TotientAsymptotic.fixed_model_band_exception_bound line 15