OAI/Computability/UniqueGames/PCP/InitialGraphLemmas.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

The initial finite constraint graph of an arbitrary concrete 3CNF formula. Clause and variable vertices use one eight-element alphabet. Variable labels are the canonical triples (bit, false, false); clause labels are arbitrary triples. Every incidence has two directed darts, including repeated names. A tautological dummy loop keeps the graph nonempty for empty formulas.

Name compaction precedes the public construction. The resulting vertex count is at most 4*m+1, and the dart count is exactly 6*m+1. Unsatisfiability gives an inverse-size gap, not a constant gap. No PCP theorem is assumed or claimed.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.Label line 37
  2. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.Vertex line 38
  3. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.Dart line 39
  4. instance OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.slotFintype line 41
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.card_slot line 45
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.card_label line 46
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.variableVertex line 49
  8. def OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.clauseVertex line 50
  9. def OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.dummyVertex line 51
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.dummyDart line 52
  11. instance OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.vertexNonempty line 54
  12. instance OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.dartNonempty line 55
  13. def OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.reverse line 57
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.reverse_involutive line 61
  15. def OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.reverseEquiv line 67
  16. def OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.tail line 73
  17. def OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.toClauseAnswer line 78
  18. def OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.fromClauseAnswer line 79
  19. def OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.variableLabel line 80
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.to_fromClauseAnswer line 82
  21. def OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.variableValid line 86
  22. def OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.incidenceAccept line 89
  23. def OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.predicate line 95
  24. def OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.raw line 100
  25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.raw_forward line 111
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.incidenceAccept_true line 116
  27. def OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.honestLabeling line 123
  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.incidence_honest line 128
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.raw_completeness line 136
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.clauseAnswer_eq_of_slots line 145
  31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.raw_reflects line 154
  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.raw_satisfiable_iff line 173
  33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.card_vertex line 176
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.card_dart line 180
  35. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.CompactVertex line 185
  36. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.CompactDart line 186
  37. def OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.build line 188
  38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.build_satisfiable_iff line 191
  39. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.build_vertex_bound line 195
  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.build_dart_count line 201
  41. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.build_initial_gap line 207

    Source documentation

    The initial inverse-size gap follows from the original unsatisfiability, without a PCP, bounded-degree, or constant-gap premise.

    theorem build_initial_gap (F : Formula) (unsat : ¬ F.Satisfiable)
    (labeling : CompactVertex F → Label) : 1 ≤ (build F).rejectionCount labeling := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.CompactVertex, OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.Label, OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.build

  42. theorem OAI.UniqueGamesTheorem.Foundations.PCP.InitialGraph.build_inverse_size_gap line 213
  43. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.bit line 237
  44. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.hits line 241
  45. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.mean line 244
  46. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.bit_nonneg line 246
  47. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.bit_sq line 250
  48. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.bit_mul line 254
  49. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.bit_mono line 258
  50. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.hits_nonneg line 266
  51. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.mean_nonneg line 269
  52. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.mean_hits line 272
  53. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.second_moment_eq line 276
  54. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.mean_witness_sq_le line 284
  55. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringMoment.rejection_lower_bound line 316
  56. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringNumeric.min_density_ratio line 353

    Source documentation

    A bounded nonnegative coefficient gives the required ratio bound both below and above the cutoff 1/t.

    theorem min_density_ratio (ε C k t : ℝ)
    (hε : 0 < ε) (hC : 0 < C) (hk : 0 ≤ k)
    (ht : 0 < t) (hkt : k ≤ t) :
    min ε (1 / t) / (C + 1) ≤ ε / (C + k * ε) := by
…
  57. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringNumeric.count_moment_ratio_lower line 382

    Source documentation

    A positive natural count supplies 0 ≤ m - 1. After cancelling the positive mass m*ε, the ratio of moments dominates a constant times min ε (1/t). No sign condition on α is needed for its fourth power.

    theorem count_moment_ratio_lower (α ε C t : ℝ) (m : ℕ)
    (hm : 0 < m) (hε : 0 < ε) (hC : 0 < C) (ht : 0 < t)
    (hmt : (m : ℝ) - 1 ≤ t) :
    (α ^ 4 * (m : ℝ) / (C + 1)) * min ε (1 / t) ≤
      (α ^ 2 * (m : ℝ) * ε) ^ 2 /
        ((m : ℝ) * ε * (C + ((m : ℝ) - 1) * ε)) := by
…
  58. structure OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.PortGraph line 417
  59. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.Edge line 421
  60. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.Walk line 422
  61. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.next line 426
  62. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.rot_rot line 428
  63. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.walkEnd line 431
  64. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.walkEnd_nil line 435
  65. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.walkEnd_cons line 437
  66. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.walkEnd_append line 440
  67. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.splitHead line 447

    Source documentation

    Exposes the first dart and the independent remaining port word.

    def splitHead (V D : Type*) (n : Nat) :
    Walk V D (n + 1) ≃ ((V × D) × (Fin n → D)) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.Walk

  68. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.rotateHead line 459

    Source documentation

    Advance across the first edge while retaining its reverse port.

    def rotateHead (G : PortGraph V D) (n : Nat) : Walk V D (n + 1) ≃ Walk V D (n + 1) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.PortGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.Walk

  69. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.rotateHead_vertex line 463
  70. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.rotateHead_zero line 466
  71. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.rotateHead_succ line 469
  72. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.permutePorts line 474

    Source documentation

    Relabeling time coordinates is a bijection on actual port words.

    def permutePorts {t : Nat} (σ : Fin t ≃ Fin t) : Walk V D t ≃ Walk V D t where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.Walk

  73. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.wordEnd line 488
  74. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.endpoint line 492
  75. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.natCard_walk line 495
  76. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.headTailEquiv line 499
  77. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.advanceTail line 510
  78. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.edgeAt line 514

    Source documentation

    The dart at the indicated time, computed by the actual preceding steps.

    def edgeAt (G : PortGraph V D) :
    (n : Nat) → Walk V D (n + 1) → Fin (n + 1) → Edge V D
  | 0, w, _ => (w.1, w.2 0)
  | n + 1, w, k => Fin.cases (w.1, w.2 0)
      (fun j => edgeAt G n (advanceTail G w) j) k

/-- Isolate any actual path edge. Previously traversed ports are replaced by
their arrival ports, so the change of coordinates remains invertible. -/

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.PortGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.Walk, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.Edge, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.advanceTail

  79. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.pivotEquiv line 522

    Source documentation

    Isolate any actual path edge. Previously traversed ports are replaced by their arrival ports, so the change of coordinates remains invertible.

    def pivotEquiv (G : PortGraph V D) :
    (n : Nat) → Fin (n + 1) →
      (Walk V D (n + 1) ≃ (Edge V D × (Fin n → D)))
  | 0, _ => splitHead V D 0
  | n + 1, k => Fin.cases (splitHead V D (n + 1))
      (fun j => (rotateHead G (n + 1)).trans
        ((headTailEquiv V D (n + 1)).trans
          ((Equiv.prodCongr (pivotEquiv G n j) (Equiv.refl D)).trans
            (headTailEquiv (Edge V D) D n).symm))) k

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.PortGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.Walk, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.Edge, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.splitHead, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.rotateHead, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.headTailEquiv

  80. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.pivotEquiv_fst line 532
  81. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.edgeAt_port line 546
  82. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.pivotEquiv_zero_apply line 562
  83. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.pivotEquiv_succ_apply line 566
  84. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.projectedFiberEquiv line 573
  85. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.projectedEventEquiv line 585
  86. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.natCard_edgeAt_fiber line 604

    Source documentation

    Every fixed dart has exactly the same number of path realizations.

    theorem natCard_edgeAt_fiber (G : PortGraph V D) (n : Nat) (k : Fin (n + 1))
    (a : Edge V D) :
    Nat.card {w : Walk V D (n + 1) // edgeAt G n w k = a} = Nat.card D ^ n := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.PortGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.Edge, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.Walk, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.edgeAt

  87. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.natCard_edgeAt_event line 614

    Source documentation

    The exact event count underlying the uniform-pivot probability law.

    theorem natCard_edgeAt_event (G : PortGraph V D) (n : Nat) (k : Fin (n + 1))
    (P : Edge V D → Prop) :
    Nat.card {w : Walk V D (n + 1) // P (edgeAt G n w k)} =
      Nat.card {a : Edge V D // P a} * Nat.card D ^ n := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.PortGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.Edge, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.Walk, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.edgeAt

  88. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.leftFromPivot line 624
  89. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.rightFromPivot line 630
  90. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.leftFromPivot_zero line 637
  91. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.rightFromPivot_zero line 641
  92. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.leftFromPivot_actual line 646
  93. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringWalks.rightFromPivot_actual line 665
  94. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.Cloud line 707

    Source documentation

    The darts departing a specified vertex.

    abbrev Cloud (G : ConstraintGraph V E A) (v : V) := {e : E // G.tail e = v}

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph

  95. def OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.cloudIndexEquiv line 709
  96. def OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.cloudRotation line 719
  97. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.cloudRotation_involutive line 724
  98. def OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.innerRotation line 732

    Source documentation

    Conjugate the disjoint union of cloud rotations into global dart coordinates.

    def innerRotation (G : ConstraintGraph V E A)
    (H : ∀ v, PortGraph (Cloud G v) D) : (E × D) ≃ (E × D) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.Cloud

  99. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.innerRotation_involutive line 736
  100. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.innerRotation_tail line 744
  101. def OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.replacementStep line 751

    Source documentation

    Internal ports rotate inside a cloud; the extra port reverses an old dart.

    def replacementStep (G : ConstraintGraph V E A)
    (H : ∀ v, PortGraph (Cloud G v) D) : E × (D ⊕ Unit) → E × (D ⊕ Unit)
  | (e, Sum.inl d) =>
      let p := innerRotation G H (e, d)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.Cloud, OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.innerRotation

  102. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.replacementStep_involutive line 758
  103. def OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.replacementPortGraph line 770
  104. def OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.replacementGraph line 780

    Source documentation

    The equality constraints and inherited original constraints on the actual rotation.

    def replacementGraph [DecidableEq A] (G : ConstraintGraph V E A)
    (H : ∀ v, PortGraph (Cloud G v) D) :
    ConstraintGraph E (E × (D ⊕ Unit)) A where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.Cloud

  105. def OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.liftLabel line 796
  106. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.replacement_satisfied_inl line 799
  107. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.replacement_satisfied_inr line 809
  108. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.replacement_complete line 815
  109. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.replacement_satisfiable line 825
  110. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.rejectionCount_eq_sum line 831
  111. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.replacement_rejectionCount line 840

    Source documentation

    Lifted labels reject precisely one external dart for each rejected original dart.

    theorem replacement_rejectionCount [Fintype E] [Fintype D] [DecidableEq A]
    (G : ConstraintGraph V E A) (H : ∀ v, PortGraph (Cloud G v) D)
    (labeling : V → A) :
    (replacementGraph G H).rejectionCount (liftLabel G labeling) =
      G.rejectionCount labeling := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.Cloud, OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.replacementGraph, OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.liftLabel

  112. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.PaddedDart line 852

    Source documentation

    Additional darts are attached to their specified original vertex.

    abbrev PaddedDart (_G : ConstraintGraph V E A) (dummy : V → Type*) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph

  113. def OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.paddedOwner line 855
  114. def OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.paddedReverse line 860
  115. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.paddedReverse_involutive line 864
  116. def OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.paddedGraph line 874

    Source documentation

    Dummy darts are self-reversing loops with an always-accepting constraint.

    def paddedGraph (G : ConstraintGraph V E A) (dummy : V → Type*) :
    ConstraintGraph V (PaddedDart G dummy) A where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.PaddedDart

  117. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.padded_satisfied_inl line 888
  118. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.padded_satisfied_inr line 893
  119. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.padded_complete line 897
  120. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.padded_satisfiable line 905
  121. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.card_paddedDart line 910
  122. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.padded_rejectionCount line 916
  123. def OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.paddedReplacementPortGraph line 926
  124. def OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.paddedReplacementGraph line 931
  125. theorem OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.paddedReplacement_rejectionCount line 937
  126. def OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.noDummyEquiv line 947

    Source documentation

    Omitting all dummy darts recovers exactly the original dart set.

    def noDummyEquiv (G : ConstraintGraph V E A) :
    PaddedDart G (fun _ : V => Empty) ≃ E where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.DegreeReplacement.PaddedDart