OAI/Computability/UniqueGames/PCP/PoweringLabelsLemmas.lean

GitHub source file

128 declarations, 0 contain sorry, 0 declared as axioms

Full-radius local opinions use a common alphabet indexed by bounded port addresses. Every opinion is decoded through a fixed address selector; arbitrary alphabet symbols need not agree on colliding addresses.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.PortWords line 30
  2. instance OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.finitePortWords line 32
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.Ball line 36
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.wordToBall line 39
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.wordToBall_surjective line 42
  6. instance OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.finiteBall line 49
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.card_portWords line 53
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.card_ball_le line 57
  9. structure OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.AddressSelector line 64
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.classicalSelector line 68
  11. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.scanWitness line 74

    Source documentation

    Executable first-match search, with a proof that a match is present.

    def scanWitness {A : Type*} (p : A → Prop) [DecidablePred p] :
    (xs : List A) → (∃ a ∈ xs, p a) → {a // p a}
  | [], h => False.elim (by simp at h)
  | a :: xs, h =>
    if ha : p a then ⟨a, ha⟩ else
      scanWitness p xs (by
        obtain ⟨b, hb, hp⟩ := h
…
  12. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.listSelector line 87

    Source documentation

    A concrete complete address list supplies a computational selector. Its length depends on the degree and radius, not on the ambient vertex count.

    def listSelector [DecidableEq V] (G : PortGraph V D) (t : Nat) (v : V)
    (addresses : List (PortWords D t)) (complete : ∀ w, w ∈ addresses) :
    AddressSelector G t v where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.PortWords, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.AddressSelector

  13. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.PaddedLabel line 98
  14. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.encode line 100
  15. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.decode line 103
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.decode_encode line 106
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.decode_surjective line 113
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.encode_injective line 117
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.decoded_word_collision line 124
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringLabels.card_paddedLabel line 130
  21. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringAddresses.allWords line 157

    Source documentation

    All words of a specified length, ordered first by their head port.

    def allWords (d : Nat) : (n : Nat) → List (Fin n → Fin d)
  | 0 => [Fin.elim0]
  | n + 1 => (List.finRange d).flatMap fun a =>
      (allWords d n).map fun p => Fin.cases a p
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringAddresses.mem_allWords line 162
  23. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringAddresses.allAddresses line 179

    Source documentation

    The complete address list, including the unique empty word.

    def allAddresses (d t : Nat) : List (PortWords (Fin d) t) :=
…
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringAddresses.mem_allAddresses line 183
  25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringAddresses.length_allWords line 191
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringAddresses.length_allAddresses line 202

    Source documentation

    The selector's search-list bound depends only on degree and radius.

    theorem length_allAddresses (d t : Nat) :
    (allAddresses d t).length = ∑ n : Fin (t + 1), d ^ n.val := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringAddresses.allAddresses

  27. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringAddresses.finitePortSelector line 209

    Source documentation

    A fully executable selector from the explicit bounded address list.

    def finitePortSelector {d : Nat} [DecidableEq V] (G : PortGraph V (Fin d))
    (t : Nat) (v : V) : AddressSelector G t v :=
…
  28. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringDecoding.mass line 228
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringDecoding.mass_sum line 233
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringDecoding.exists_mode line 248
  31. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringDecoding.mode line 254
  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringDecoding.mode_max line 257
  33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringDecoding.mode_mass_lower line 261
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringDecoding.exists_letter_mass_lower line 272
  35. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.addressCount line 298

    Source documentation

    The number of words with length at most t, including the empty word.

    def addressCount (d t : Nat) : Nat := ∑ i : Fin (t + 1), d ^ i.val
  36. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.reverseWordEquiv line 302

    Source documentation

    Reverse the digit positions before using the little-endian arithmetic encoding from mathlib. Both directions are the same executable operation.

    def reverseWordEquiv (d n : Nat) : (Fin n → Fin d) ≃ (Fin n → Fin d) where
…
  37. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.wordEquiv line 309

    Source documentation

    An executable bijection from fixed-length port words to their ranks.

    def wordEquiv (d n : Nat) : (Fin n → Fin d) ≃ Fin (d ^ n) :=
…
  38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.wordEquiv_val line 312
  39. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.addressEquiv line 316

    Source documentation

    Arithmetic prefix sums give a rank for every bounded-length address.

    def addressEquiv (d t : Nat) : PortWords (Fin d) t ≃ Fin (addressCount d t) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.addressCount

  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.addressEquiv_val line 320
  41. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.paddedLabelEquiv line 330

    Source documentation

    A padded label is a base-q integer whose digits are indexed by the explicit bounded-address equivalence.

    def paddedLabelEquiv (d t q : Nat) :
    PaddedLabel (Fin d) t (Fin q) ≃ Fin (q ^ addressCount d t) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.addressCount

  42. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.paddedLabelEquiv_val line 335
  43. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.orientationEquiv line 341

    Source documentation

    False and true are the adjacent orientation digits zero and one.

    def orientationEquiv : Bool ≃ Fin 2 := finTwoEquiv.symm
  44. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.orientationEquiv_false line 343
  45. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.orientationEquiv_true line 344
  46. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.dartBlockEquiv line 347

    Source documentation

    A vertex's block consists of one adjacent orientation pair per word.

    def dartBlockEquiv (d n : Nat) :
    ((Fin (n + 1) → Fin d) × Bool) ≃ Fin (2 * d ^ (n + 1)) :=
…
  47. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.dartBlockEquiv_val line 352
  48. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.dartVertexEquiv line 359

    Source documentation

    The tuple permutation putting the vertex before its word and orientation.

    def dartVertexEquiv (vertices d n : Nat) :
    (Bool × (Fin vertices × (Fin (n + 1) → Fin d))) ≃
      (Fin vertices × ((Fin (n + 1) → Fin d) × Bool)) where
…
  49. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.dartEquiv line 368

    Source documentation

    Executable vertex-major dart numbering, with adjacent orientations.

    def dartEquiv (vertices d n : Nat) :
    (Bool × (Fin vertices × (Fin (n + 1) → Fin d))) ≃
      Fin (2 * vertices * d ^ (n + 1)) :=
…
  50. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.dartEquiv_val line 377
  51. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.dartEquiv_true_eq_false_add_one line 387

    Source documentation

    The true orientation immediately follows the false orientation.

    theorem dartEquiv_true_eq_false_add_one (vertices d n : Nat) (v : Fin vertices)
    (p : Fin (n + 1) → Fin d) :
    (dartEquiv vertices d n (true, (v, p))).val =
      (dartEquiv vertices d n (false, (v, p))).val + 1 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.dartEquiv

  52. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.encodeWord line 394
  53. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.decodeWord line 395
  54. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.decodeWord_encodeWord line 397
  55. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.encodeWord_decodeWord line 400
  56. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.encodeAddress line 403
  57. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.decodeAddress line 406
  58. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.decodeAddress_encodeAddress line 409
  59. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.encodeAddress_decodeAddress line 412
  60. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.encodeLabel line 415
  61. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.decodeLabel line 418
  62. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.decodeLabel_encodeLabel line 422
  63. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.encodeLabel_decodeLabel line 425
  64. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.decodeLabel_apply line 428
  65. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.encodeDart line 432
  66. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.decodeDart line 436
  67. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.decodeDart_encodeDart line 440
  68. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.encodeDart_decodeDart line 445
  69. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.card_words line 450
  70. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.card_addresses line 453
  71. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.card_labels line 457
  72. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.card_darts line 461
  73. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringEnumeration.length_allAddresses line 466
  74. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReach.ReachLE line 491
  75. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReach.reach_refl line 494
  76. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReach.reach_mono line 497
  77. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReach.reach_prepend line 502
  78. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReach.reversePorts line 510

    Source documentation

    Reversal records each arrival port, not the original outgoing port.

    def reversePorts (G : PortGraph V D) : V → List D → List D
  | _, [] => []
  | v, d :: ds => reversePorts G (next G v d) ds ++ [(G.rot (v, d)).2]
  79. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReach.reversePorts_length line 514
  80. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReach.walkEnd_reversePorts line 520
  81. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReach.wordEnd_eq_walkEnd_ofFn line 531
  82. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReach.reach_reverse line 541
  83. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReach.tail_reach line 554

    Source documentation

    The actual prefix places each traversed edge's tail in the start ball.

    theorem tail_reach (G : PortGraph V D) :
    ∀ (n : Nat) (w : Walk V D (n + 1)) (k : Fin (n + 1)),
      ReachLE G (n + 1) w.1 (edgeAt G n w k).1 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReach.ReachLE

  84. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReach.head_reach_endpoint line 569

    Source documentation

    The suffix proceeds from the traversed edge's head to the walk endpoint.

    theorem head_reach_endpoint (G : PortGraph V D) :
    ∀ (n : Nat) (w : Walk V D (n + 1)) (k : Fin (n + 1)),
      ReachLE G (n + 1) (G.rot (edgeAt G n w k)).1 (endpoint G w) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReach.ReachLE

  85. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReach.tailFromStart line 583
  86. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReach.headFromEnd line 587
  87. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReach.tailFromStart_val line 591
  88. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringReach.headFromEnd_val line 595
  89. structure OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.Verifier line 620
  90. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.Label line 624
  91. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.Vertex line 625
  92. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.Dart line 626
  93. def OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.response line 630
  94. def OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.zeroSlot line 633
  95. def OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.decodeRight line 635
  96. def OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.encodeRight line 637
  97. theorem OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.decode_encodeRight line 639
  98. def OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.canonicalSlot line 642
  99. theorem OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.canonicalSlot_query line 645
  100. def OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.RepeatedConsistent line 649
  101. instance OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.repeatedConsistentDecidable line 652
  102. def OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.LeftValid line 658
  103. instance OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.leftValidDecidable line 661
  104. def OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.incidenceAccept line 667
  105. def OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.reverse line 672
  106. theorem OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.reverse_involutive line 674
  107. def OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.reverseEquiv line 678
  108. def OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.tail line 684
  109. def OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.predicate line 688
  110. def OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.graph line 693
  111. theorem OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.edgeSatisfied_eq_incidence line 703
  112. def OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.honestLabeling line 711
  113. theorem OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.honest_leftValid line 715
  114. theorem OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.honest_incidence line 722
  115. theorem OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.perfect_completeness line 733
  116. theorem OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.satisfiable_of_verifier_satisfiable line 741
  117. def OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.decodedAssignment line 749
  118. theorem OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.incidenceAccept_true line 752
  119. theorem OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.all_incidences_imply_event line 761
  120. theorem OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.rejected_event_forces_slot line 776
  121. def OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.rejectedEvents line 794
  122. def OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.verifierRejectionCount line 797
  123. theorem OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.rejection_count_bound line 802

    Source documentation

    Every rejected event contributes two distinct rejected darts, one in each orientation. A classical witness is used only in this counting proof.

    theorem rejection_count_bound [Fintype E] [DecidableEq X]
    (T : Verifier E X q) (positive : 0 < q) (labeling : Vertex E X → Label q) :
    2 * verifierRejectionCount T (decodedAssignment positive labeling) ≤
      (graph T positive).rejectionCount labeling := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.Verifier, OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.Label, OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.verifierRejectionCount, OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.decodedAssignment, OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.graph

  124. theorem OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.card_label line 831
  125. theorem OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.card_vertex line 834
  126. theorem OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.card_dart line 838
  127. theorem OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.gap_transfer line 842
  128. theorem OAI.UniqueGamesTheorem.Foundations.PCP.QueryIncidence.six_query_alphabet line 857