OAI/Computability/UniqueGames/Machines/FinalCNFTableAdapter.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Structural conversion to the generic 64-label table format

The fixed and generic formats store exactly the same fields in the same order. Conversion maps the row structure, keeping each endpoint, reversal index, and relation vector unchanged. In particular, the serialized input bits are equal, so the generic table lookup machine applies to the actual final-converter input.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericRow line 20
  2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericRow_tail line 24
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericRow_reverseIndex line 27
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericRow_relation line 30
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericRows line 33
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericRows_get line 36
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericRows_reverseAt line 40
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericRows_acceptsAt line 47
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericRows_valid line 54
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable line 63

    Source documentation

    No row is recomputed, reordered, or selected by an abstract enumeration.

    def genericTable (table : GraphTables.Table) : GenericGraphTables.Table 64 where
…
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable_vertices line 69
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable_darts line 72
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable_row line 75
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable_tail line 78
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable_reverseIndex line 83
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable_relation line 88
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericRow_words line 93
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable_rowList line 96
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable_tableWords line 102
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable_tableBits line 109

    Source documentation

    The shared lookup machine consumes exactly the original serialized input.

    @[simp] theorem genericTable_tableBits (table : GraphTables.Table) :
    GenericGraphTables.tableBits (genericTable table) = GraphTables.tableBits table := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable

  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_tail line 113
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_reverse line 117
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_head line 122
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_accepts line 128
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable_headIndex line 133
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable_headValue line 137
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable_headValue_tableGraph line 143
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTableAdapter.genericTable_pattern_relation line 149