OAI/NumberTheory/TwoPoint/Walks/RetainedEligibility.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

On the actual tuple and padding pools, canonical pair membership agrees with the original bin eligibility, including inside the density cut.

  1. lemma OAI.TwoPointCorrelations.canonicalTraceFamily_pair_on_pool line 13
  2. lemma OAI.TwoPointCorrelations.integerEdgeKeep_congr_eligible line 23
  3. lemma OAI.TwoPointCorrelations.retainedNumericalEdge_congr_eligible line 35
  4. lemma OAI.TwoPointCorrelations.retainedPrimePrefix_congr_eligible line 47