OAI/Computability/UniqueGames/PCP/OverlayLemmas.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

Overlay a regular constraint graph with an actual regular port graph whose new constraints always accept. The port sets are disjoint, so all original rejected darts are retained exactly. The averaging operator is the actual degree-weighted mixture of the two graph averages.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.originalPortGraph line 30
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.rotate line 34
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.rotate_involutive line 39
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.portGraph line 48
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.portGraph_rot_inl line 56
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.portGraph_rot_inr line 61
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.constraintGraph line 67

    Source documentation

    Keep the original tests and add always-accepting tests on the overlay ports.

    def constraintGraph (G : ConstraintGraph V (V × D) A) (H : PortGraph V E) :
    ConstraintGraph V (V × (D ⊕ E)) A where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph

  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.constraintGraph_tail line 81
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.constraintGraph_portGraph line 84
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.edgeSatisfied_inl line 88
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.edgeSatisfied_inr line 98
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.complete line 102
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.satisfiable_iff line 112
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.rejectionCount_eq line 125

    Source documentation

    Every labeling rejects exactly the same number of darts before and after overlay.

    theorem rejectionCount_eq [Fintype V] [Fintype D] [Fintype E]
    (G : ConstraintGraph V (V × D) A) (H : PortGraph V E)
    (htail : G.tail = Prod.fst) (labeling : V → A) :
    (constraintGraph G H).rejectionCount labeling = G.rejectionCount labeling := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.constraintGraph

  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.card_ports line 134
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.card_darts line 137
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.operator_mix line 148

    Source documentation

    The normalized graph average weights the components by their actual port counts.

    theorem operator_mix [Nonempty D] [Nonempty E]
    (G : PortGraph V D) (H : PortGraph V E) (f : V → ℝ) (v : V) :
    averagingOperator (portGraph G H) f v =
      (Fintype.card D : ℝ) / ((Fintype.card D : ℝ) + Fintype.card E) *
        averagingOperator G f v +
      (Fintype.card E : ℝ) / ((Fintype.card D : ℝ) + Fintype.card E) *
        averagingOperator H f v := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.portGraph

  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.energy_convex_mix line 168

    Source documentation

    Convexity of the squared energy, proved pointwise before taking the finite mean.

    theorem energy_convex_mix (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1)
    (f g : V → ℝ) :
    energy (fun v => a * f v + b * g v) ≤ a * energy f + b * energy g := by
…
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.energy_bound line 185

    Source documentation

    Actual overlay contraction from the supplied graph's spectral bound and the proved energy contraction of an arbitrary reversible regular graph.

    theorem energy_bound [Nonempty V] [Nonempty D] [Nonempty E]
    (G : PortGraph V D) (H : PortGraph V E) (lambda : ℝ)
    (certificate : SpectralCertificate H lambda) (f : V → ℝ) (hf : mean f = 0) :
    energy (averagingOperator (portGraph G H) f) ≤
      ((Fintype.card D : ℝ) + (Fintype.card E : ℝ) * lambda ^ 2) /
        ((Fintype.card D : ℝ) + Fintype.card E) * energy f := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.portGraph

  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.energy_bound_three_quarters line 222

    Source documentation

    With one more original port than overlay ports, a half-spectral overlay has squared contraction at most three quarters.

    theorem energy_bound_three_quarters [Nonempty V]
    (G : PortGraph V D) (H : PortGraph V E)
    (hdegree : Fintype.card D = Fintype.card E + 1) (hpositive : 1 ≤ Fintype.card E)
    (certificate : SpectralCertificate H (1 / 2 : ℝ))
    (f : V → ℝ) (hf : mean f = 0) :
    energy (averagingOperator (portGraph G H) f) ≤ (3 / 4 : ℝ) * energy f := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.portGraph

  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.spectralCertificate_seven_eighths line 241
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.constraintGraph_spectralCertificate line 255

    Source documentation

    The certificate belongs to the exact underlying graph of the overlaid constraints.

    theorem constraintGraph_spectralCertificate [Nonempty V]
    (G : ConstraintGraph V (V × D) A) (H : PortGraph V E)
    (hdegree : Fintype.card D = Fintype.card E + 1) (hpositive : 1 ≤ Fintype.card E)
    (certificate : SpectralCertificate H (1 / 2 : ℝ)) :
    SpectralCertificate (originalPortGraph (constraintGraph G H)) (7 / 8 : ℝ) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.originalPortGraph, OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.constraintGraph

  23. def OAI.UniqueGamesTheorem.Foundations.PCP.LazyConstraint.constraintGraph line 282
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazyConstraint.constraintGraph_tail line 294
  25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazyConstraint.constraintGraph_reverse line 297
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazyConstraint.constraintGraph_portGraph line 300
  27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazyConstraint.edgeSatisfied_false line 304
  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazyConstraint.edgeSatisfied_true line 308
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazyConstraint.complete line 317
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazyConstraint.complete_iff line 327
  31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazyConstraint.satisfiable_iff line 338
  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazyConstraint.rejectionCount_eq line 347

    Source documentation

    The equality holds for every labeling, including nonsatisfying ones.

    theorem rejectionCount_eq [Fintype V] [Fintype D]
    (G : ConstraintGraph V (V × D) A) (htail : G.tail = Prod.fst)
    (labeling : V → A) :
    (constraintGraph G).rejectionCount labeling = G.rejectionCount labeling := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.LazyConstraint.constraintGraph

  33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazyConstraint.card_ports line 356
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazyConstraint.card_darts line 360
  35. theorem OAI.UniqueGamesTheorem.Foundations.PCP.LazyConstraint.rejection_density_eq_half line 366

    Source documentation

    The actual normalized rejection probability is halved. The identity also holds for empty dart types, using the field's totalized division.

    theorem rejection_density_eq_half [Fintype V] [Fintype D]
    (G : ConstraintGraph V (V × D) A) (htail : G.tail = Prod.fst)
    (labeling : V → A) :
    ((constraintGraph G).rejectionCount labeling : ℝ) /
        (Fintype.card (V × (Bool × D)) : ℝ) =
      ((G.rejectionCount labeling : ℝ) / (Fintype.card (V × D) : ℝ)) / 2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.LazyConstraint.constraintGraph

  36. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.listEquiv line 400

    Source documentation

    An explicit complete list supplies both directions of a finite encoding. The forward direction searches the list; its inverse performs list indexing.

    def listEquiv {α : Type*} [BEq α] [LawfulBEq α] (xs : List α)
    (nodup : xs.Nodup) (complete : ∀ a, a ∈ xs) : α ≃ Fin xs.length where
…
  37. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.listEquiv_val line 409
  38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.listEquiv_symm_apply line 413
  39. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudDarts line 418

    Source documentation

    Retain the input dart order and test only the stored tail index.

    def cloudDarts (t : Table) (v : Fin t.vertices) : List (Fin t.darts) :=
…
  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.mem_cloudDarts line 421
  41. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_nodup line 425
  42. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_sublist line 431

    Source documentation

    Filtering preserves the original ordering, including repeated row values at different dart indices.

    theorem cloudDarts_sublist (t : Table) (v : Fin t.vertices) :
    (cloudDarts t v).Sublist (List.finRange t.darts) := List.filter_sublist

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudDarts

  43. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudSize line 434
  44. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudSize_le_darts line 436
  45. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudSelect line 441

    Source documentation

    Read the original dart stored at a valid local cloud index.

    def cloudSelect (t : Table) (v : Fin t.vertices) (i : Fin (cloudSize t v)) :
    Cloud (semantics t) v :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudSize

  46. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudRank line 447

    Source documentation

    Find the local index of an original dart belonging to this cloud.

    def cloudRank (t : Table) (v : Fin t.vertices) (e : Cloud (semantics t) v) :
    Fin (cloudSize t v) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudSize

  47. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_val line 452
  48. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudRank_val line 456
  49. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_cloudRank line 460
  50. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudRank_cloudSelect line 465
  51. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudEquiv line 472

    Source documentation

    This equivalence contains executable rank and select functions, including when both its domain and codomain are empty.

    def cloudEquiv (t : Table) (v : Fin t.vertices) :
    Cloud (semantics t) v ≃ Fin (cloudSize t v) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudSize

  52. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudSize_eq_card_cloud line 479
  53. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_eq_nil_iff line 483
  54. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudSize_eq_zero_iff line 487
  55. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.sum_cloudSize line 491
  56. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.oldCloudIndex line 501

    Source documentation

    An original global dart carries its own owner and executable local rank.

    def oldCloudIndex (t : Table) (e : Fin t.darts) :
    Fin (cloudSize t t.rows[e].tail) := cloudRank t t.rows[e].tail ⟨e, rfl⟩

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudSize, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudRank

  57. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_oldCloudIndex line 504
  58. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.PaddedCloud line 510

    Source documentation

    Padding counts are supplied as executable natural-valued data, without choosing enumerations of the semantic clouds by their cardinalities.

    abbrev PaddedCloud (t : Table) (padding : Fin t.vertices → Nat)
    (v : Fin t.vertices) :=
…
  59. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.paddedOld line 514
  60. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.paddedNew line 518
  61. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.paddedCloudEquiv line 523

    Source documentation

    Local padded order: old cloud indices first, then increasing dummy index.

    def paddedCloudEquiv (t : Table) (padding : Fin t.vertices → Nat)
    (v : Fin t.vertices) : PaddedCloud t padding v ≃ Fin (cloudSize t v + padding v) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.PaddedCloud, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.cloudSize

  62. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank line 529
  63. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect line 533
  64. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_rank line 537
  65. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_select line 542
  66. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_old line 547
  67. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_new line 552
  68. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_old_val line 557
  69. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_new_val line 562
  70. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_castAdd line 567
  71. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_natAdd line 579
  72. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.card_paddedCloud line 585
  73. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.levelLoop line 598
  74. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.levelLoop_level_le line 605

    Source documentation

    At most fuel continuing iterations can increment the exponent.

    theorem levelLoop_level_le (g k fuel e s : Nat) :
    (levelLoop g k fuel e s).1 ≤ e + fuel := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.levelLoop

  75. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.levelLoop_power line 617

    Source documentation

    The carried size remains the exact power of the carried exponent.

    theorem levelLoop_power (g k fuel e : Nat) :
    (levelLoop g k fuel e (g ^ e)).2 =
      g ^ (levelLoop g k fuel e (g ^ e)).1 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.levelLoop

  76. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.levelLoop_covers line 628
  77. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.levelLoop_le_of_covering_power line 645

    Source documentation

    The search never passes an exponent whose power already covers the request. This remains true even without a sufficient fuel budget.

    theorem levelLoop_le_of_covering_power (g k fuel e j : Nat)
    (he : e ≤ j) (hj : k ≤ g ^ j) :
    (levelLoop g k fuel e (g ^ e)).1 ≤ j := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.levelLoop

  78. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.searchResult line 662
  79. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.boundedLevel line 666

    Source documentation

    An executable exponent, computed with at most k multiplications.

    def boundedLevel (k : Nat) : Nat := (searchResult k).1

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.searchResult

  80. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.paddedSize line 669

    Source documentation

    The algorithm returns the power it has already computed.

    def paddedSize (k : Nat) : Nat := (searchResult k).2

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.searchResult

  81. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.boundedLevel_zero line 671
  82. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.paddedSize_zero line 673
  83. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.boundedLevel_le_input line 675
  84. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.paddedSize_power line 679
  85. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.le_paddedSize line 684
  86. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.boundedLevel_eq_level line 689

    Source documentation

    The bounded multiplication loop computes the existing ceiling logarithm.

    theorem boundedLevel_eq_level (k : Nat) :
    boundedLevel k = ExpanderFamily.level k := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.boundedLevel, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.level

  87. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.paddedSize_eq_size line 699
  88. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.boundedLevel_le_of_le_power line 704

    Source documentation

    The returned exponent is the least exponent whose power covers k.

    theorem boundedLevel_le_of_le_power {k j : Nat}
    (h : k ≤ ExpanderFamily.growth ^ j) : boundedLevel k ≤ j := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.growth, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.boundedLevel

  89. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.paddedSize_positive line 709
  90. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.paddedSize_bounds line 715

    Source documentation

    Positive cloud sizes and positive whole-graph vertex counts increase by at most the single fixed growth factor.

    theorem paddedSize_bounds {k : Nat} (hk : 0 < k) :
    k ≤ paddedSize k ∧ paddedSize k ≤ ExpanderFamily.growth * k := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.paddedSize, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.growth

  91. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.cloudPaddedSize line 721

    Source documentation

    Empty clouds remain empty; nonempty clouds use the geometric family.

    def cloudPaddedSize (k : Nat) : Nat := if k = 0 then 0 else paddedSize k

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.paddedSize

  92. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_zero line 723
  93. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_of_pos line 725
  94. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_bounds line 729
  95. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.table_vertexCount_eq_paddedSize line 738

    Source documentation

    The executable table family has exactly the size returned by the loop.

    theorem table_vertexCount_eq_paddedSize (k : Nat) :
    ExpanderTables.vertexCount (Expanders.baseDegree * Expanders.baseDegree)
        (boundedLevel k) = paddedSize k := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.vertexCount, OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.baseDegree, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.boundedLevel, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.paddedSize

  96. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.family_row_count_at_size line 749