OAI/Computability/UniqueGames/PCP/PreprocessingPaddingOffsets.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The executable dummy numbering is the sum of earlier cloud sizes plus the local dummy index. This connects the actual list search in vertexOrder with unary prefix-sum routines, without changing the chosen enumeration.

  1. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingOffsets.idxOf_map_injective line 16
  2. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingOffsets.sigma_idxOf line 26
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingOffsets.offset line 53
  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingOffsets.sigma_length line 56
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingOffsets.paddingOrder_val line 62
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingOffsets.vertexOrder_dummy_val line 70
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingOffsets.offset_zero line 77
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingOffsets.offset_all line 80