OAI/Computability/MaxCut/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.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.row line 17
  2. abbrev OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.trueRelation line 18
  3. def OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.oldReverseMap line 20
  4. def OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.expanderReverseMap line 21
  5. def OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.oldRow line 23
  6. def OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.expanderRow line 29
  7. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.relation_ext_inline_PreprocessingOverlayWords line 34
  8. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.row_overlay_old line 41
  9. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.row_overlay_expander line 54
  10. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.oldRow_reverse_val line 70
  11. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.expanderRow_reverse_val line 78
  12. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.oldRow_words line 86
  13. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.expanderRow_words line 93
  14. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.ofFn_overlayPorts line 103
  15. def OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.vertexRows line 109
  16. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.vertexRows_length line 113
  17. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.flatRows_overlay line 117
  18. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.vertexRows_words line 127
  19. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.tableWords_overlay line 150
  20. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.tableBits_overlay line 155
  21. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayWords.rotationWords_vertices line 162

    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.MaxCutGames.Foundations.PCP.ExpanderTables.Table, OAI.MaxCutGames.Foundations.PCP.ExpanderTableWords.rotationWords, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.reverseIndex, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.rowIndex