OAI/Computability/UniqueGames/PCP/PreprocessingOverlayWords.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Exact stored-row and codec expansion of the executable overlay. Within each vertex block, all original ports precede all expander ports.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.row line 18
  2. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.trueRelation line 19
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.oldReverseMap line 21
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.expanderReverseMap line 22
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.oldRow line 24
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.expanderRow line 30
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.relation_ext line 35
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.row_overlay_old line 42
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.row_overlay_expander line 55
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.oldRow_reverse_val line 71
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.expanderRow_reverse_val line 79
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.oldRow_words line 87
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.expanderRow_words line 94
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.ofFn_overlayPorts line 104
  15. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.vertexRows line 110
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.vertexRows_length line 114
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.flatRows_overlay line 118
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.vertexRows_words line 128
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.tableWords_overlay line 151
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.tableBits_overlay line 156
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayWords.rotationWords_vertices line 163

    Source documentation

    The expander's raw stream has the same exact per-vertex port order.

    theorem rotationWords_vertices (H : ExpanderTables.Table n e) :
    ExpanderTableWords.rotationWords H =
      (List.ofFn fun v : Fin n => List.ofFn fun p : Fin e =>
        (ExpanderTables.reverseIndex H (ExpanderTables.rowIndex n e (v, p))).val).flatten := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.rotationWords, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.reverseIndex, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.rowIndex