OAI/Computability/MaxCut/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.MaxCutGames.Foundations.PCP.PreprocessingPaddingOffsets.idxOf_map_injective_inline_PreprocessingPaddingOffsets line 15
  2. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingOffsets.sigma_idxOf line 25
  3. def OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingOffsets.offset line 52
  4. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingOffsets.sigma_length line 55
  5. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingOffsets.paddingOrder_val line 61
  6. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingOffsets.vertexOrder_dummy_val line 69
  7. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingOffsets.offset_zero line 76
  8. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingOffsets.offset_all line 79