OAI/NumberTheory/TotientAsymptotic/LocalPrimeRoughness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

At each actual residual index the geometric head-prime minimum exceeds its fourth-power normality cutoff.

  1. theorem OAI.TotientAsymptotic.local_geometric_prime_above_normality line 13
  2. theorem OAI.TotientAsymptotic.local_bad_suffix_head_roughness line 30
  3. theorem OAI.TotientAsymptotic.local_geometric_primes_three line 52
  4. lemma OAI.TotientAsymptotic.ordered_prime_product_largest line 65