OAI/NumberTheory/TwoPoint/Bounds/PrimeAlphabetSize.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The full forced-step alphabet includes all bounded padding divisors. Its size still fits the polynomial exponential budget of finite-law comparison; no eligibility restriction is needed for this count.

  1. lemma OAI.TwoPointCorrelations.boundedPaddingDivisor_real_upper line 14
  2. lemma OAI.TwoPointCorrelations.boundedPaddingDivisors_card line 38
  3. lemma OAI.TwoPointCorrelations.actual_prime_alphabet_size line 59