OAI/Computability/UniqueGames/Machines/FinalCNFStream.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Exact row enumeration and input/output stream identities for the concrete final-CNF machine. Rows occur in stored order, including repeated rows.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents line 17

    Source documentation

    The actual unprocessed suffix of the finite table's stored row indices.

    def remainingEvents (table : GraphTables.Table) (r : Nat) : List (Fin table.darts) :=
…
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.processedEvents line 20
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.inputStream line 23
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.outputStream line 26
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_zero line 31
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_length line 35
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_done line 39
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_cons line 43
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_zero line 50
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_done line 53
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_succ line 57
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.processed_append_remaining line 64
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.inputStream_nil line 68
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.inputStream_cons line 70
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.inputStream_append line 75
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.outputStream_nil line 80
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.outputStream_cons line 83
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.outputStream_append line 89
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.inputStream_remaining_cons line 95
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.outputStream_remaining_cons line 102
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.outputStream_processed_succ line 110
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.inputStream_split line 119
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.outputStream_split line 125
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.encodeWords_flatMap_rows line 131
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowList_eq_finRange_map line 137
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.inputStream_all line 144

    Source documentation

    The stream starts at exactly the row suffix left by the checked header phase.

    theorem inputStream_all (table : GraphTables.Table) :
    inputStream table (List.finRange table.darts) = tableRowsBits (genericTable table) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.inputStream, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.tableRowsBits

  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.inputStream_remaining_zero line 155
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.outputStream_accumulator_succ line 160

    Source documentation

    Pushing a row's reversed emission realizes extension of the forward prefix.

    theorem outputStream_accumulator_succ (plan : Plan) (table : GraphTables.Table)
    (r : Nat) (h : r < table.darts) (header : List Bool) :
    (plan.flatMap (Emitter.commandBits (rowOperands table ⟨r, h⟩)
      (rowRelation table ⟨r, h⟩))).reverse ++
        (header ++ outputStream plan table (processedEvents table r)).reverse =
      (header ++ outputStream plan table (processedEvents table (r + 1))).reverse := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowOperands, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowRelation, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.outputStream, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.processedEvents