OAI/NumberTheory/TwoPoint/Walks/AttachedWitnessCatalog.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The residue test also records the attachment positions on the main path.

  1. abbrev OAI.TwoPointCorrelations.WitnessRecord line 13
  2. lemma OAI.TwoPointCorrelations.witnessAttachment_cost line 16
  3. lemma OAI.TwoPointCorrelations.witnessRecord_cost line 37
  4. theorem OAI.TwoPointCorrelations.recorded_witness_record line 51
  5. theorem OAI.TwoPointCorrelations.eventually_attached_witness_decay line 64