OAI/Computability/UniqueGames/PCP/PreprocessingLazyWords.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Exact codec expansion of the executable lazy graph table. Each vertex contributes its d always-accepting selfloops, followed by its d stored constraints with the reverse field changed by the displayed div/mod map.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.row line 19
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.trueRelation line 23
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.stayRow line 25
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.moveRow line 28
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.reverseMap line 35

    Source documentation

    The machine's fixed-degree numerical map for an old reverse-row index.

    def reverseMap (d j : Nat) : Nat := 2 * d * (j / d) + d + j % d
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.relation_ext line 37
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.row_lazy_stay line 44
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.row_lazy_move line 57
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.stayRow_reverse_val line 70
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.moveRow_reverse_val line 75
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.relationWords_true line 83
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.stayRow_words line 87
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.moveRow_words line 93
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.ofFn_rowIndex line 101

    Source documentation

    Finite mixed-radix indexing agrees with the actual row-vector order.

    theorem ofFn_rowIndex {α : Type*} (f : Fin (n * d) → α) :
    List.ofFn f = (List.ofFn fun v : Fin n =>
      List.ofFn fun p : Fin d => f (rowIndex n d (v, p))).flatten := by
…
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.flatRows_list line 115
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.ofFn_lazyPorts line 123

    Source documentation

    Boolean false precedes true in the executable lazy port numbering.

    theorem ofFn_lazyPorts {α : Type*} (f : Fin (2 * d) → α) :
    List.ofFn f = List.ofFn (fun p => f (lazyPorts d (false, p))) ++
      List.ofFn (fun p => f (lazyPorts d (true, p))) := by
…
  17. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.vertexRows line 136
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.vertexRows_length line 140
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.flatRows_lazy line 146

    Source documentation

    Every stored lazy row, with no permutation or multiset quotient.

    theorem flatRows_lazy (table : PortTables.Table n d) :
    (flatRows (lazy table)).toList = (List.ofFn (vertexRows table)).flatten := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.vertexRows

  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.vertexRows_words line 156
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.tableWords_lazy line 177

    Source documentation

    The full existing word codec, including both graph header fields.

    theorem tableWords_lazy (table : PortTables.Table n d) :
    PortTables.tableWords (lazy table) =
      [n, n * (2 * d)] ++ (List.ofFn (vertexRows table)).flatten.flatMap rowWords := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.tableWords, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.vertexRows

  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.tableBits_lazy line 183

    Source documentation

    The same statement for the exact unary-delimited Boolean input/output codec.

    theorem tableBits_lazy (table : PortTables.Table n d) :
    PortTables.tableBits (lazy table) =
      encodeWords ([n, n * (2 * d)] ++
        (List.ofFn (vertexRows table)).flatten.flatMap rowWords) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.tableBits, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLazyWords.vertexRows