OAI/Computability/MaxCut/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.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.row line 17
  2. def OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.trueRelation line 21
  3. def OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.stayRow line 23
  4. def OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.moveRow line 26
  5. def OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.reverseMap line 33

    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.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.relation_ext_inline_PreprocessingLazyWords line 35
  7. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.row_lazy_stay line 42
  8. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.row_lazy_move line 55
  9. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.stayRow_reverse_val line 68
  10. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.moveRow_reverse_val line 73
  11. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.relationWords_true line 81
  12. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.stayRow_words line 85
  13. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.moveRow_words line 91
  14. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.ofFn_rowIndex line 99

    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.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.flatRows_list line 113
  16. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.ofFn_lazyPorts line 121

    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.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.vertexRows line 134
  18. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.vertexRows_length line 138
  19. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.flatRows_lazy line 144

    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.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.vertexRows

  20. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.vertexRows_words line 154
  21. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.tableWords_lazy line 175

    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.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PortTables.tableWords, OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.vertexRows

  22. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.tableBits_lazy line 181

    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.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PortTables.tableBits, OAI.MaxCutGames.Foundations.PCP.PreprocessingLazyWords.vertexRows