OAI/NumberTheory/TwoPoint/Bounds/NumericalWitnessEncoding.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual numerical witness families are covered by the prime-slot catalog.

  1. lemma OAI.TwoPointCorrelations.LabeledPrimeWord.realizes_support_covered line 13
  2. lemma OAI.TwoPointCorrelations.wordPrimeSupport_mono line 26
  3. lemma OAI.TwoPointCorrelations.PrimeWordEncoding.tuple_support_covered line 32
  4. theorem OAI.TwoPointCorrelations.PrimeWordEncoding.covers_witnesses line 45
  5. theorem OAI.TwoPointCorrelations.numerical_witness_sum_le_encoding line 72