OAI/NumberTheory/TwoPoint/Walks/ClosedTraceEncoding.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual closed-pair catalog has length 2*k, as in the trace bounds.

  1. lemma OAI.TwoPointCorrelations.columnTupleWord_reindex line 11
  2. def OAI.TwoPointCorrelations.closedTraceEncoding line 20
  3. theorem OAI.TwoPointCorrelations.closedTraceEncoding_word line 29
  4. theorem OAI.TwoPointCorrelations.closedTraceEncoding_injective line 41