OAI/NumberTheory/TwoPoint/Bounds/IntegerClosedCatalog.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A fixed-length numerical closed word remembers both forced matrix paths. Only their starting site and external copy indices remain outside this code.

  1. theorem OAI.TwoPointCorrelations.integerStepWord_injective line 12
  2. def OAI.TwoPointCorrelations.integerClosedWordCode line 27
  3. theorem OAI.TwoPointCorrelations.integerClosedWordCode_injective line 31