OAI/Computability/UniqueGames/PCP/GenericGraphTables.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

Executable directed graph tables over a fixed finite alphabet

The alphabet size q is fixed by the encoding, not encoded as a variable input field. The header stores vertex and directed-dart counts. Each ordered dart row stores its tail, reverse index, and every q*q predicate bit in order b+q*a. All fields use the existing unary natural-word codec. Decoding validates graph laws and preserves loops and repeated darts. Size bounds count the complete serialized table and make no running-time assertion.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Label line 22
  2. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.RelationTable line 23
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.relationIndex line 28

    Source documentation

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

    def relationIndex (q : Nat) : (Label q) × (Label q) ≃ Fin (q * q) := finProdFinEquiv

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

  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.relationIndex_val line 30
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.relationAt line 33
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.relationOf line 36
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.relationAt_relationOf line 39
  8. structure OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.DartRow line 44

    Source documentation

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

    structure DartRow (q vertices darts : Nat) where
…
  9. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Rows line 49
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.reverseAt line 51
  11. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.acceptsAt line 54
  12. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Valid line 58

    Source documentation

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

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

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

  13. instance OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.(instance at line 62) line 62
  14. structure OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table line 66
  15. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.rowList line 73

    Source documentation

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

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

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

  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.rowList_length line 75
  17. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics line 79

    Source documentation

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

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

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

  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics_reverse line 90
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics_tail line 93
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics_accepts line 96
  21. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.graphRows line 99
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.reverseAt_graphRows line 102
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.acceptsAt_graphRows line 107
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.graphRows_valid line 112
  25. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.ofGraph line 120
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics_ofGraph_reverse line 123
  27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics_ofGraph_tail line 128
  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics_ofGraph_accepts line 134
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics_ofGraph_edgeSatisfied line 139
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.constraintGraph_ext line 144
  31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics_ofGraph line 159

    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 q)) : semantics (ofGraph G) = G := by
…

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

  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics_ofGraph_rejectionCount line 168
  33. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.enumeratedGraph line 176

    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 q)) :
    ConstraintGraph (Fin n) (Fin m) (Label q) where
…

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

  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.enumeratedGraph_edgeSatisfied line 192
  35. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.enumeratedGraph_rejectionCount line 201

    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 q)) (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.GenericGraphTables.Label, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.enumeratedGraph

  36. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.ofEnumeratedGraph line 213
  37. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.bitWord line 217
  38. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.parseBit line 219
  39. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.parseBit_bitWord line 224
  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.parseBits_bitWords line 227
  41. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.relationWords line 233
  42. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.relationWords_length line 235
  43. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.parseRelation line 238
  44. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.parseRelation_encoded line 244
  45. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.rowWords line 251
  46. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.parseRow line 254
  47. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.parseRow_encoded line 262
  48. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.parseRows line 270
  49. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.parseRows_encoded line 278
  50. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.tableWords line 284
  51. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.tableBits line 287
  52. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.decodeTableWords line 289
  53. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.decodeTableWords_encoded line 300
  54. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.decodeTableBits line 308
  55. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.decodeTableBits_encoded line 311
  56. def OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.encoding line 316

    Source documentation

    A concrete encoding for the fixed alphabet, suitable for the existing TM2 computation interface.

    def encoding (q : Nat) : Computability.Encoding (Table q) Bool where
…

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

  57. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.tableBits_injective line 321
  58. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.rowWords_length line 323
  59. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.rowsWords_length line 329
  60. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.tableWords_length line 335
  61. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.tableWords_length_le_bits line 342

    Source documentation

    At least one unary delimiter is stored for every field, including all (q * q) entries of every predicate table.

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

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

  62. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.relationBits_length_le line 347
  63. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.rowBits_length_le line 355
  64. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.rowsBits_length_le line 364
  65. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.tableBits_length_le line 376

    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 q)) :
    (tableBits table).length ≤ table.vertices + table.darts + 2 +
      table.darts * (table.vertices + table.darts + (2 * (q * q))) := by
…

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

  66. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.vertices_le_tableBits_length line 385
  67. theorem OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.darts_le_tableBits_length line 391