OAI/NumberTheory/TwoPoint/Walks/ProhibitedFamilyWitnesses.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The literal minimal-word catalog discharges the numerical witness-family hypotheses.

  1. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.catalog_pairs line 15
  2. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.catalog_admissible line 19
  3. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.catalog_whole_squarefree line 25
  4. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.catalog_tuple_card line 29
  5. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.catalog_prime_support line 33
  6. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.catalog_padding_excluded line 47