OAI/NumberTheory/Ostmann/Construction/InitialWordCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Explicit original word and cell coordinates for the signed atom schedule

  1. def OAI.Ostmann.initialWordSize line 11
  2. def OAI.Ostmann.positiveWordConstituentEquiv line 15
  3. def OAI.Ostmann.signedConstituentEquiv line 26
  4. def OAI.Ostmann.positiveWordTupleEquiv line 36
  5. def OAI.Ostmann.initialWordTupleEquiv line 42
  6. theorem OAI.Ostmann.initialWordTupleEquiv_positive line 50
  7. theorem OAI.Ostmann.initialWordTupleEquiv_negative line 56
  8. theorem OAI.Ostmann.initialWordTupleEquiv_character line 62
  9. theorem OAI.Ostmann.wordCopyEquiv_positive_word line 79
  10. theorem OAI.Ostmann.wordCopyEquiv_negative_word line 88
  11. theorem OAI.Ostmann.initialWordTuple_positive_word line 97
  12. theorem OAI.Ostmann.initialWordTuple_negative_word line 104