OAI/Computability/UniqueGames/PCP/GraphTables.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

Executable directed-dart tables for the fixed 64-label alphabet

The header gives vertex and dart counts. Every dart has one ordered row: tail index, reverse-dart index, and 4096 Boolean predicate entries. Entry b + 64 * a is the predicate at labels (a,b). All fields, including bits as 0/1 words, use the existing zero-delimited unary natural-word codec.

The decoder checks all index bounds, row counts, predicate lengths, reverse involution, predicate transpose, and absence of trailing fields. Directed rows preserve loops, self-reversing darts, and repeated constraint occurrences. The size theorems concern the full encoded table, not a machine runtime.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Label line 28
  2. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.RelationTable line 29
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.relationIndex line 32

    Source documentation

    The fixed row-major ordering of the complete predicate table.

    def relationIndex : Label × Label ≃ Fin 4096 := finProdFinEquiv

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Label

  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.relationIndex_val line 34
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.relationAt line 37
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.relationOf line 40
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.relationAt_relationOf line 43
  8. structure OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.DartRow line 48

    Source documentation

    The row itself is finite data; index bounds are checked while parsing.

    structure DartRow (vertices darts : Nat) where
…
  9. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Rows line 53
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.reverseAt line 55
  11. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.acceptsAt line 58
  12. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Valid line 62

    Source documentation

    The two graph laws are decidable finite checks on the stored rows.

    def Valid {n m : Nat} (rows : Rows n m) : Prop :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Rows

  13. instance OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.(instance at line 66) line 66
  14. structure OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table line 70
  15. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.rowList line 77

    Source documentation

    The ordered list serialized by the codec. Equal rows remain separate.

    def rowList (table : Table) : List (DartRow table.vertices table.darts) := table.rows.toList

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

  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.rowList_length line 79
  17. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics line 83

    Source documentation

    Decode validated finite data into the actual constraint-graph semantics.

    def semantics (table : Table) : ConstraintGraph (Fin table.vertices) (Fin table.darts) Label where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Label

  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics_reverse line 94
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics_tail line 97
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics_accepts line 100
  21. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.graphRows line 103
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.reverseAt_graphRows line 106
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.acceptsAt_graphRows line 111
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.graphRows_valid line 116
  25. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.ofGraph line 124
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics_ofGraph_reverse line 127
  27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics_ofGraph_tail line 132
  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics_ofGraph_accepts line 138
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics_ofGraph_edgeSatisfied line 143
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.constraintGraph_ext line 148
  31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics_ofGraph line 163

    Source documentation

    Complete semantic graph roundtrip, including its actual reversal map.

    @[simp] theorem semantics_ofGraph {n m : Nat}
    (G : ConstraintGraph (Fin n) (Fin m) Label) : semantics (ofGraph G) = G := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Label, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.ofGraph

  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics_ofGraph_rejectionCount line 172
  33. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.enumeratedGraph line 180

    Source documentation

    Explicit enumerations determine every vertex name, dart position, and predicate label. No hidden choice of a graph representation is made.

    def enumeratedGraph {V E A : Type*} {n m : Nat} (G : ConstraintGraph V E A)
    (vertexOrder : V ≃ Fin n) (dartOrder : E ≃ Fin m) (labelOrder : A ≃ Label) :
    ConstraintGraph (Fin n) (Fin m) Label where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Label

  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.enumeratedGraph_edgeSatisfied line 196
  35. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.enumeratedGraph_rejectionCount line 205

    Source documentation

    Every directed occurrence contributes once before and after enumeration.

    theorem enumeratedGraph_rejectionCount {V E A : Type*} [Fintype E] {n m : Nat}
    (G : ConstraintGraph V E A) (vertexOrder : V ≃ Fin n) (dartOrder : E ≃ Fin m)
    (labelOrder : A ≃ Label) (labeling : V → A) :
    (enumeratedGraph G vertexOrder dartOrder labelOrder).rejectionCount
      (fun v => labelOrder (labeling (vertexOrder.symm v))) = G.rejectionCount labeling := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Label, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.enumeratedGraph

  36. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.ofEnumeratedGraph line 217
  37. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.bitWord line 221
  38. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.parseBit line 223
  39. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.parseBit_bitWord line 228
  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.parseBits_bitWords line 231
  41. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.relationWords line 237
  42. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.relationWords_length line 239
  43. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.parseRelation line 242
  44. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.parseRelation_encoded line 248
  45. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.rowWords line 255
  46. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.parseRow line 258
  47. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.parseRow_encoded line 266
  48. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.parseRows line 274
  49. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.parseRows_encoded line 282
  50. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.tableWords line 288
  51. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.tableBits line 291
  52. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.decodeTableWords line 293
  53. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.decodeTableWords_encoded line 304
  54. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.decodeTableBits line 312
  55. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.decodeTableBits_encoded line 315
  56. def OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.encoding line 320

    Source documentation

    A concrete encoding suitable for the existing TM2 computation interface.

    def encoding : Computability.Encoding Table Bool where
…

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

  57. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.tableBits_injective line 325
  58. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.rowWords_length line 327
  59. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.rowsWords_length line 330
  60. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.tableWords_length line 336
  61. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.tableWords_length_le_bits line 343

    Source documentation

    At least one unary delimiter is stored for every field, including all 4096 entries of every predicate table.

    theorem tableWords_length_le_bits (table : Table) :
    2 + 4098 * table.darts ≤ (tableBits table).length := by
…

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

  62. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.relationBits_length_le line 348
  63. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.rowBits_length_le line 356
  64. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.rowsBits_length_le line 365
  65. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.tableBits_length_le line 377

    Source documentation

    Full unary size bound: headers, both bounded indices in every row, and every Boolean predicate entry are counted. This is not a runtime assertion.

    theorem tableBits_length_le (table : Table) :
    (tableBits table).length ≤ table.vertices + table.darts + 2 +
      table.darts * (table.vertices + table.darts + 8192) := by
…

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

  66. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.vertices_le_tableBits_length line 386
  67. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.darts_le_tableBits_length line 392