OAI/Computability/UniqueGames/PCP/Table.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.rowFromDart line 12

   Source documentation

   One directed occurrence, without merging repeated queries or equal rows.

   def rowFromDart (input : GenericGraphTables.Table q)
       (dart : QueryIncidence.Dart (AlphabetGraph.Event (Fin input.darts) (Fin q)) 6) :
       GraphTables.DartRow (Enumeration.vertexCount input.vertices input.darts q)
         (Enumeration.dartCount input.darts q) :=
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.Dart, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.Event, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.DartRow, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.vertexCount, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.dartCount

2. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.rows line 31

   Source documentation

   The row number decodes to precisely one event/slot/orientation occurrence.

   def rows (input : GenericGraphTables.Table q) :
       GraphTables.Rows (Enumeration.vertexCount input.vertices input.darts q)
         (Enumeration.dartCount input.darts q) :=
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Rows, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.vertexCount, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.dartCount

3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.rows_at line 37
4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.rows_reverseIndex line 44

   Source documentation

   Reversal changes only the occurrence's orientation, preserving event and slot.

   theorem rows_reverseIndex (input : GenericGraphTables.Table q)
       (index : Fin (Enumeration.dartCount input.darts q)) :
       (rows input)[index].reverseIndex =
         Enumeration.dartEquiv input.darts q
           (((Enumeration.dartEquiv input.darts q).symm index).1,
             !((Enumeration.dartEquiv input.darts q).symm index).2) := by
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.dartCount, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.rows, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv

5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.dartRow_ext line 52
6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.relation_ext line 62
7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.rowFromDart_eq_graphRow line 74

   Source documentation

   The three stored fields agree with the actual alphabet graph at this dart.

   theorem rowFromDart_eq_graphRow (input : GenericGraphTables.Table q)
       (dart : QueryIncidence.Dart (AlphabetGraph.Event (Fin input.darts) (Fin q)) 6) :
       rowFromDart input dart =
         { tail := Enumeration.vertexEquiv input.vertices input.darts q
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.Dart, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.Event, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.rowFromDart, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv

8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.rows_eq_graphRows line 114

   Source documentation

   Equality of the full row vector, including all multiplicities and reversal indices.

   theorem rows_eq_graphRows (input : GenericGraphTables.Table q) :
       rows input = GraphTables.graphRows
         (GraphTables.enumeratedGraph (AlphabetGraph.graph (GenericGraphTables.semantics input))
           (Enumeration.vertexEquiv input.vertices input.darts q)
           (Enumeration.dartEquiv input.darts q) Enumeration.labelEquiv) := by
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.rows, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.graphRows, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.enumeratedGraph, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.graph, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv

9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.rows_valid line 125
10. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.build line 130

    Source documentation

    Actual executable output table. Its validity proof is erased at execution.

    def build (input : GenericGraphTables.Table q) : GraphTables.Table where
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table

11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.build_vertices line 136
12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.build_darts line 139
13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.table_rows_congr line 142
14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.semantics_rows_congr line 148
15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.build_eq_ofEnumeratedGraph line 156

    Source documentation

    Exact table equality in the explicit enumerations, without a representation choice.

    theorem build_eq_ofEnumeratedGraph (input : GenericGraphTables.Table q) :
        build input =
          GraphTables.ofEnumeratedGraph (AlphabetGraph.graph (GenericGraphTables.semantics input))
            (Enumeration.vertexEquiv input.vertices input.darts q)
            (Enumeration.dartEquiv input.darts q) Enumeration.labelEquiv := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.build, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.ofEnumeratedGraph, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.graph, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv

16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.semantics_build line 165

    Source documentation

    Full decoded graph equality, including reversal, endpoints, and every predicate bit.

    theorem semantics_build (input : GenericGraphTables.Table q) :
        GraphTables.semantics (build input) =
          GraphTables.enumeratedGraph (AlphabetGraph.graph (GenericGraphTables.semantics input))
            (Enumeration.vertexEquiv input.vertices input.darts q)
            (Enumeration.dartEquiv input.darts q) Enumeration.labelEquiv := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.build, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.enumeratedGraph, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.graph, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv

17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.decode_build line 174

    Source documentation

    Encoding and decoding the executable output recovers the full intended table.

    theorem decode_build (input : GenericGraphTables.Table q) :
        GraphTables.decodeTableBits (GraphTables.tableBits (build input)) =
          some (GraphTables.ofEnumeratedGraph
            (AlphabetGraph.graph (GenericGraphTables.semantics input))
            (Enumeration.vertexEquiv input.vertices input.darts q)
            (Enumeration.dartEquiv input.darts q) Enumeration.labelEquiv) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.decodeTableBits, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.tableBits, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.build, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.ofEnumeratedGraph, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.graph, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv

18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.edgeSatisfied_build line 182
19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.rejectionCount_build line 195
20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.perfect_completeness line 206
21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.gap_transfer line 221

    Source documentation

    The gap statement transfers to every labeling of the actual numbered table.

    theorem gap_transfer [Nonempty (Fin q)] (input : GenericGraphTables.Table q) (a b : Nat)
        (source : ∀ labeling : Fin input.vertices → Fin q,
          a * input.darts ≤ b * (GenericGraphTables.semantics input).rejectionCount labeling)
        (labeling : Fin (build input).vertices → GraphTables.Label) :
        a * (build input).darts ≤
          (b * 12288) * (GraphTables.semantics (build input)).rejectionCount labeling := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.build, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Label, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics

22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.rowList_eq_ordered line 246

    Source documentation

    The serialized row list follows the same explicit occurrence order as the vector.

    theorem rowList_eq_ordered (input : GenericGraphTables.Table q) :
        GraphTables.rowList (build input) =
          (Enumeration.ordered (Enumeration.dartEquiv input.darts q)).map
            (rowFromDart input) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.rowList, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.build, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.ordered, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.rowFromDart

23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.tableWords_eq_ordered line 256

    Source documentation

    Complete output words: two headers followed by every ordered row block.

    theorem tableWords_eq_ordered (input : GenericGraphTables.Table q) :
        GraphTables.tableWords (build input) =
          [Enumeration.vertexCount input.vertices input.darts q,
            Enumeration.dartCount input.darts q] ++
            (Enumeration.ordered (Enumeration.dartEquiv input.darts q)).flatMap
              (fun dart => GraphTables.rowWords (rowFromDart input dart)) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.tableWords, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.build, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.vertexCount, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.dartCount, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.ordered, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.rowWords, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.rowFromDart

24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.rowList_length line 265
25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.tableWords_length line 269
26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.tableBits_length_le line 274