OAI/Computability/UniqueGames/PCP/AlphabetGraphLemmas.lean

GitHub source file

124 declarations, 0 contain sorry, 0 declared as axioms

Real gap and exact size of the alphabet graph

The gap bound is obtained directly from the two checked rejection-count inequalities. The finite graph's size is linear in the old vertices and darts, with an explicit coefficient determined only by the old alphabet cardinality.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.Address line 20
  2. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.LocalEvent line 22
  3. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.Event line 25
  4. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.legal line 29
  5. instance OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.legalDecidable line 32
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.restrictTape line 36
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.extendTape line 39
  8. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.globalizeQuery line 43
  9. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.verifier line 48
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.vertexBlock line 55
  11. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.edgeOracle line 58
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.oracleAnswer_globalize line 63
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.response_eq_local line 75
  14. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.eventReject line 88
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.eventReject_eq_local line 93
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.expect_prod line 106
  17. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.localAverage line 111
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.expect_restrict_five line 115

    Source documentation

    Iterating the checked one-tape restriction identity preserves independence.

    theorem expect_restrict_five {B : Type*} [Fintype B] [DecidableEq B]
    (p : B → Prop) [DecidablePred p]
    (h : ({b // p b} → Bool) → ({b // p b} → Bool) → ({b // p b} → Bool) →
      ({b // p b} → Bool) → ({b // p b} → Bool) → ℝ) :
    (𝔼 f : B → Bool, 𝔼 g : B → Bool, 𝔼 r₀ : B → Bool,
      𝔼 r₁ : B → Bool, 𝔼 r₂ : B → Bool,
        h (UniformRestriction.restrict p f) (UniformRestriction.restrict p g)
          (UniformRestriction.restrict p r₀) (UniformRestriction.restrict p r₁)
          (UniformRestriction.restrict p r₂)) =
    𝔼 f : {b // p b} → Bool, 𝔼 g : {b // p b} → Bool,
      𝔼 r₀ : {b // p b} → Bool, 𝔼 r₁ : {b // p b} → Bool,
        𝔼 r₂ : {b // p b} → Bool, h f g r₀ r₁ r₂ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.UniformRestriction.restrict

  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.localAverage_eq_tester line 153

    Source documentation

    Five independent full tapes restrict to five independent uniform legal tapes.

    theorem localAverage_eq_tester (G : ConstraintGraph V E A)
    (assignment : Address V E A → Bool) (e : E) :
    localAverage G assignment e = AlphabetReduction.edgeTesterReject (G.accepts e)
      (vertexBlock assignment (G.tail e)) (vertexBlock assignment (G.head e))
      (edgeOracle G assignment e) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.Address, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.localAverage, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetReduction.edgeTesterReject, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.vertexBlock, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.edgeOracle

  20. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.average line 171
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.average_eq_testers line 176
  22. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.decodedLabeling line 185
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.local_gap line 188
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.average_gap line 205
  25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.expect_rejection_eq_count line 213
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.average_eq_count line 226
  27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.card_event line 233
  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.card_localEvent line 239

    Source documentation

    This factor depends only on the old alphabet, never on a dart predicate.

    theorem card_localEvent :
    Fintype.card (LocalEvent A) =
      4 * (2 * 2 ^ Fintype.card A) * (2 ^ (Fintype.card A * Fintype.card A)) ^ 5 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.LocalEvent

  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.card_address line 246
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.rejection_count_bound line 254

    Source documentation

    The actual event count has a uniform loss of 2048, with no edge-dependent sample multiplicities. This count statement also permits an empty dart type.

    theorem rejection_count_bound [Fintype E] (G : ConstraintGraph V E A)
    (assignment : Address V E A → Bool) :
    Fintype.card (LocalEvent A) * G.rejectionCount (decodedLabeling assignment) ≤
      2048 * QueryIncidence.verifierRejectionCount (verifier G) assignment := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.Address, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.LocalEvent, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.decodedLabeling, OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.verifierRejectionCount, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.verifier

  31. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.honestAssignment line 281
  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.honest_vertexBlock line 286
  33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.honest_edgeOracle line 290
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.honest_event line 299
  35. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.graph line 311
  36. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.perfect_completeness line 316
  37. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.gap_transfer line 323

    Source documentation

    The combined tester and incidence losses are 2048 × 6 = 12288.

    theorem gap_transfer [Fintype E] [DecidableEq V] [DecidableEq E]
    (G : ConstraintGraph V E A) (a b : Nat)
    (source : ∀ labeling : V → A,
      a * Fintype.card E ≤ b * G.rejectionCount labeling)
    (labeling : QueryIncidence.Vertex (Event E A) (Address V E A) → QueryIncidence.Label 6) :
    a * Fintype.card (QueryIncidence.Dart (Event E A) 6) ≤
      (b * 12288) * (graph G).rejectionCount labeling := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.Event, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.Address, OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.Label, OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.Dart, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.graph

  38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.alphabet_card line 349
  39. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.OutputVertex line 367
  40. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.OutputDart line 370
  41. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.localEventFactor line 373

    Source documentation

    The number of local verifier events for an alphabet with q symbols.

    def localEventFactor (q : Nat) : Nat :=
…
  42. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.vertexFactor line 376
  43. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.dartFactor line 378
  44. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.sizeFactor line 380
  45. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.sizeFactor_positive line 382
  46. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.gap_transfer_real line 391

    Source documentation

    Real gaps transfer without rational approximation, including an empty old dart type. The loss is exactly 2048 * 6 = 12288.

    theorem gap_transfer_real [Fintype E] [DecidableEq V] [DecidableEq E]
    (G : ConstraintGraph V E A) (eps : ℝ) (_eps_nonnegative : 0 ≤ eps)
    (source : ∀ labeling : V → A,
      eps * (Fintype.card E : ℝ) ≤ (G.rejectionCount labeling : ℝ))
    (labeling : OutputVertex V E A → QueryIncidence.Label 6) :
    (eps / 12288) * (Fintype.card (OutputDart E A) : ℝ) ≤
      ((AlphabetGraph.graph G).rejectionCount labeling : ℝ) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.OutputVertex, OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.Label, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.OutputDart, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.graph

  47. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.card_output_vertex line 430
  48. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.card_output_dart line 439
  49. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.card_output_total line 445
  50. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.card_output_total_le line 454

    Source documentation

    One coefficient depending only on the alphabet bounds the actual total number of output vertices and darts.

    theorem card_output_total_le :
    Fintype.card (OutputVertex V E A) + Fintype.card (OutputDart E A) ≤
      sizeFactor (Fintype.card A) * (Fintype.card V + Fintype.card E) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.OutputVertex, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.OutputDart, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.sizeFactor

  51. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.card_output_vertex_le line 471
  52. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.card_output_dart_le line 476
  53. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.bitValue line 499
  54. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.boolEquiv line 501
  55. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.boolEquiv_val line 503
  56. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.productEquiv line 507

    Source documentation

    Left component first, with the right component varying fastest.

    def productEquiv {A B : Type*} {a b : Nat} (left : A ≃ Fin a) (right : B ≃ Fin b) :
    A × B ≃ Fin (a * b) :=
…
  57. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.productEquiv_val line 511
  58. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv line 518

    Source documentation

    The complete left block precedes the complete right block.

    def sumEquiv {A B : Type*} {a b : Nat} (left : A ≃ Fin a) (right : B ≃ Fin b) :
    A ⊕ B ≃ Fin (a + b) :=
…
  59. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv_inl_val line 522
  60. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv_inr_val line 526
  61. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.tapeCount line 530
  62. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.pairTapeCount line 531
  63. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.fiveTapeCount line 532
  64. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.localCount line 533
  65. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.eventCount line 534
  66. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.addressCount line 535
  67. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.vertexCount line 536
  68. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.dartCount line 537
  69. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.cubeEquiv line 541

    Source documentation

    Explicit binary rank/unrank; the inverse extracts digits by division and remainder, as supplied by the executable finFunctionFinEquiv.

    def cubeEquiv (q : Nat) : Cube (Fin q) ≃ Fin (tapeCount q) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.tapeCount

  70. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.cubeRank line 544
  71. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank line 545
  72. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank_cubeRank line 548
  73. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.cubeRank_cubeUnrank line 551
  74. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank_digit line 554
  75. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.cubeEquiv_val line 562
  76. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.pairIndex line 568
  77. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.pairIndex_val line 570
  78. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.pairCubeEquiv line 575
  79. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.pairCubeRank line 578
  80. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.pairCubeUnrank line 581
  81. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.pairCubeUnrank_pairCubeRank line 584
  82. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.pairCubeRank_pairCubeUnrank line 587
  83. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.pairCubeEquiv_val line 590
  84. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.inputCoordinateEquiv line 595
  85. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.fivePairTapesEquiv line 599
  86. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.localEventEquiv line 608
  87. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.eventEquiv line 613
  88. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv line 617
  89. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv line 622
  90. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv line 627
  91. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv line 632
  92. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv_val line 634
  93. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.inputCoordinateEquiv_val line 638
  94. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.fivePairTapesEquiv_val line 643
  95. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.localEventEquiv_val line 651
  96. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.eventEquiv_val line 660
  97. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv_inl_val line 667
  98. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv_inr_val line 674
  99. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_event_val line 681
  100. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_vertexAddress_val line 685
  101. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_edgeAddress_val line 692
  102. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv_val line 700
  103. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv_reverse_val line 708
  104. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.ordered line 715

    Source documentation

    A reusable explicit increasing-index enumeration.

    def ordered {A : Type*} {count : Nat} (order : A ≃ Fin count) : List A :=
…
  105. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.ordered_length line 718
  106. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.mem_ordered line 721
  107. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.ordered_nodup line 726
  108. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.ordered_refl line 731
  109. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.ordered_bool line 733
  110. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.ordered_trans_finCongr line 735
  111. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.ordered_product line 742

    Source documentation

    Product enumeration visits the right factor completely at each left index.

    theorem ordered_product {A B : Type*} {a b : Nat}
    (left : A ≃ Fin a) (right : B ≃ Fin b) :
    ordered (productEquiv left right) =
      (ordered left).flatMap (fun x => (ordered right).map (fun y => (x, y))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.ordered, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.productEquiv

  112. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.ordered_sum line 759

    Source documentation

    Sum enumeration puts the whole left block before the whole right block.

    theorem ordered_sum {A B : Type*} {a b : Nat}
    (left : A ≃ Fin a) (right : B ≃ Fin b) :
    ordered (sumEquiv left right) =
      (ordered left).map Sum.inl ++ (ordered right).map Sum.inr := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.ordered, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv

  113. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.localEvents line 779
  114. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.localEvents_length line 782
  115. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.ordered_event line 785
  116. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.ordered_dart line 794

    Source documentation

    Exact serialized occurrence order, including both orientations and every repeated local query: edge, local event, slot, then false and true.

    theorem ordered_dart (m q : Nat) :
    ordered (dartEquiv m q) =
      (List.finRange m).flatMap (fun edge =>
        (localEvents q).flatMap (fun event =>
          (List.finRange 6).flatMap (fun slot =>
            [(((edge, event), slot), false), (((edge, event), slot), true)]))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.ordered, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.localEvents

  117. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.card_cube line 806
  118. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.card_pairCube line 809
  119. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.card_localEvent line 813
  120. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.card_event line 817
  121. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.card_address line 821
  122. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.card_vertex line 825
  123. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.card_dart line 830
  124. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.localCount_formula line 835