OAI/Computability/MaxCut/PCP/PortTables.lean

GitHub source file

132 declarations, 0 contain sorry, 0 declared as axioms

Executable regular constraint tables on the fixed 64-label alphabet

Every pair (vertex,port) has one stored reverse index and one complete 4096-bit relation. Flat row port + ports * vertex has its tail implicitly fixed by that pair. Rotation uses the stored vector lookup, followed by the inverse row-index bijection. Loops and repeated directed occurrences remain distinct rows.

Serialization uses the existing GraphTables codec: header [vertices,darts] with darts=vertices*ports, then tail/reverse/4096 bit words per row.

  1. abbrev OAI.MaxCutGames.Foundations.PCP.PortTables.Label line 23
  2. def OAI.MaxCutGames.Foundations.PCP.PortTables.rowIndex line 25
  3. theorem OAI.MaxCutGames.Foundations.PCP.PortTables.rowIndex_val line 28
  4. structure OAI.MaxCutGames.Foundations.PCP.PortTables.Table line 32

    Source documentation

    Finite executable input data, with the two graph laws certified on lookup.

    structure Table (vertices ports : Nat) where
…
  5. def OAI.MaxCutGames.Foundations.PCP.PortTables.rotation line 44

    Source documentation

    One reverse-index lookup and the fixed mixed-radix decoding.

    def rotation (table : Table n d) (e : Fin n × Fin d) : Fin n × Fin d :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table

  6. def OAI.MaxCutGames.Foundations.PCP.PortTables.accepts line 48

    Source documentation

    Lookup of the full stored binary predicate.

    def accepts (table : Table n d) (e : Fin n × Fin d) (a b : Label) : Bool :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PortTables.Label

  7. theorem OAI.MaxCutGames.Foundations.PCP.PortTables.rowIndex_rotation line 51
  8. theorem OAI.MaxCutGames.Foundations.PCP.PortTables.rotation_involutive line 55
  9. theorem OAI.MaxCutGames.Foundations.PCP.PortTables.accepts_rotation line 61
  10. def OAI.MaxCutGames.Foundations.PCP.PortTables.portGraph line 66

    Source documentation

    The actual reversible regular port graph represented by the vectors.

    def portGraph (table : Table n d) : PortGraph (Fin n) (Fin d) where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table

  11. theorem OAI.MaxCutGames.Foundations.PCP.PortTables.portGraph_rot line 74
  12. def OAI.MaxCutGames.Foundations.PCP.PortTables.baseGraph line 78

    Source documentation

    Constraint-graph semantics, with each vertex-port pair a distinct dart.

    def baseGraph (table : Table n d) : ConstraintGraph (Fin n) (Fin n × Fin d) Label where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.PortTables.Label

  13. theorem OAI.MaxCutGames.Foundations.PCP.PortTables.baseGraph_reverse line 85
  14. theorem OAI.MaxCutGames.Foundations.PCP.PortTables.baseGraph_tail line 88
  15. theorem OAI.MaxCutGames.Foundations.PCP.PortTables.baseGraph_head line 91
  16. theorem OAI.MaxCutGames.Foundations.PCP.PortTables.baseGraph_accepts line 94
  17. def OAI.MaxCutGames.Foundations.PCP.PortTables.ofPortGraph line 98

    Source documentation

    Materialize a reversible port graph and its predicates into the fixed rows.

    def ofPortGraph (G : PortGraph (Fin n) (Fin d))
    (predicate : (Fin n × Fin d) → Label → Label → Bool)
    (htranspose : ∀ e a b, predicate (G.rot e) b a = predicate e a b) : Table n d where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Label, OAI.MaxCutGames.Foundations.PCP.PortTables.Table

  18. theorem OAI.MaxCutGames.Foundations.PCP.PortTables.rotation_ofPortGraph line 115
  19. theorem OAI.MaxCutGames.Foundations.PCP.PortTables.accepts_ofPortGraph line 122
  20. def OAI.MaxCutGames.Foundations.PCP.PortTables.flatRows line 130
  21. theorem OAI.MaxCutGames.Foundations.PCP.PortTables.reverseAt_flatRows line 134
  22. theorem OAI.MaxCutGames.Foundations.PCP.PortTables.acceptsAt_flatRows line 138
  23. theorem OAI.MaxCutGames.Foundations.PCP.PortTables.flatRows_valid line 142
  24. def OAI.MaxCutGames.Foundations.PCP.PortTables.graphTable line 149
  25. def OAI.MaxCutGames.Foundations.PCP.PortTables.tableWords line 153

    Source documentation

    Existing graph codec, with header [n,n*d] and 4098 words in every row.

    def tableWords (table : Table n d) : List Nat := GraphTables.tableWords (graphTable table)

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.GraphTables.tableWords, OAI.MaxCutGames.Foundations.PCP.PortTables.graphTable

  26. def OAI.MaxCutGames.Foundations.PCP.PortTables.tableBits line 155
  27. abbrev OAI.MaxCutGames.Foundations.PCP.PortTables.Input line 158

    Source documentation

    Variable vertex count, with the port count fixed by the input family.

    abbrev Input (ports : Nat) := (vertices : Nat) × Table vertices ports

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table

  28. def OAI.MaxCutGames.Foundations.PCP.PortTables.inputBits line 160
  29. theorem OAI.MaxCutGames.Foundations.PCP.PortTables.tableWords_eq line 162
  30. theorem OAI.MaxCutGames.Foundations.PCP.PortTables.tableWords_length line 165
  31. theorem OAI.MaxCutGames.Foundations.PCP.PortTables.vertices_le_tableBits_length line 169
  32. abbrev OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.Cloud line 195

    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.MaxCutGames.Foundations.PCP.ConstraintGraph

  33. def OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.cloudIndexEquiv line 197
  34. def OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.cloudRotation line 207
  35. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.cloudRotation_involutive line 212
  36. def OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.innerRotation line 220

    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.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.Cloud

  37. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.innerRotation_involutive line 224
  38. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.innerRotation_tail line 232
  39. def OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.replacementStep line 239

    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.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.Cloud, OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.innerRotation

  40. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.replacementStep_involutive line 246
  41. def OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.replacementPortGraph line 258
  42. def OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.replacementGraph line 268

    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.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.Cloud

  43. def OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.liftLabel line 284
  44. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.replacement_satisfied_inl line 287
  45. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.replacement_satisfied_inr line 297
  46. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.replacement_complete line 303
  47. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.replacement_satisfiable line 313
  48. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.rejectionCount_eq_sum line 319
  49. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.replacement_rejectionCount line 328

    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.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.Cloud, OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.replacementGraph, OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.liftLabel

  50. abbrev OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.PaddedDart line 340

    Source documentation

    Additional darts are attached to their specified original vertex.

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

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph

  51. def OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.paddedOwner line 343
  52. def OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.paddedReverse line 348
  53. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.paddedReverse_involutive line 352
  54. def OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.paddedGraph line 362

    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.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.PaddedDart

  55. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.padded_satisfied_inl line 376
  56. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.padded_satisfied_inr line 381
  57. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.padded_complete line 385
  58. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.padded_satisfiable line 393
  59. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.card_paddedDart line 398
  60. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.padded_rejectionCount line 404
  61. def OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.paddedReplacementPortGraph line 414
  62. def OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.paddedReplacementGraph line 419
  63. theorem OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.paddedReplacement_rejectionCount line 425
  64. def OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.noDummyEquiv line 435

    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.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.DegreeReplacement.PaddedDart

  65. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.truth line 472
  66. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.disagree line 474
  67. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.truth_nonneg line 476
  68. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.disagree_nonneg line 478
  69. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.disagree_eq line 481
  70. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.disagree_xor_le line 485
  71. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.parity line 489
  72. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.bitSign_parity line 492
  73. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.bitSign_injective line 500
  74. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.parity_xor line 504
  75. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.cubeXor_comm line 510
  76. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.cubeXor_right_twice line 515
  77. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.expect_cubeXor line 521
  78. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.distance line 536
  79. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.distance_nonneg line 539
  80. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.distance_parity line 545
  81. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.blrReject line 553
  82. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.blrReject_nonneg line 556
  83. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.blr_correlation line 563
  84. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.blrReject_fourier line 582
  85. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.blr_near_parity line 592

    Source documentation

    The actual BLR test yields a nearby parity, with no stability theorem or Fourier-structure hypothesis assumed.

    theorem blr_near_parity (F : Cube A → Bool) :
    ∃ s : Cube A, distance F (parity s) ≤ blrReject F := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AssignmentTester.distance, OAI.MaxCutGames.Foundations.PCP.AssignmentTester.parity, OAI.MaxCutGames.Foundations.PCP.AssignmentTester.blrReject

  86. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.selfCorrect line 622
  87. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.parity_selfCorrect line 625
  88. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.selfCorrect_error line 631

    Source documentation

    The two actual oracle queries recover the parity at every requested x.

    theorem selfCorrect_error (F : Cube A → Bool) (s x : Cube A) :
    (𝔼 r, disagree (selfCorrect F x r) (parity s x)) ≤ 2 * distance F (parity s) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AssignmentTester.disagree, OAI.MaxCutGames.Foundations.PCP.AssignmentTester.selfCorrect, OAI.MaxCutGames.Foundations.PCP.AssignmentTester.parity, OAI.MaxCutGames.Foundations.PCP.AssignmentTester.distance

  89. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.singleMask line 645
  90. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.flipAt line 647
  91. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.flipAt_twice line 651
  92. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.flipAt_eq_xor line 656
  93. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.expect_flipAt line 660
  94. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.walsh_singleMask line 665
  95. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.parity_singleMask line 675
  96. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.parity_flipAt line 679
  97. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.cubeAnd line 684
  98. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.andLawFailure line 686
  99. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.andLawFailure_flipAt_second line 689
  100. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.four_truth_lower_inline_AssignmentTester line 706
  101. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.parity_and_rejection line 712

    Source documentation

    Every parity involving two or more distinct coordinates violates Boolean AND with probability at least one quarter under two independent queries.

    theorem parity_and_rejection (s : Cube A) (i j : A)
    (hi : s i = true) (hj : s j = true) (hij : i ≠ j) :
    (1 : ℝ) / 4 ≤ 𝔼 f, 𝔼 g, truth (andLawFailure s f g) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AssignmentTester.truth, OAI.MaxCutGames.Foundations.PCP.AssignmentTester.andLawFailure

  102. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.truth_xor line 741
  103. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.disagree_triangle line 744
  104. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.and_disagree_transfer line 748
  105. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.andReject line 755

    Source documentation

    Six oracle queries, using three independent self-correction masks.

    def andReject (F : Cube A → Bool) : ℝ :=
…
  106. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.unitReject line 760
  107. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.inputReject line 766

    Source documentation

    One original input query and two proof-oracle queries.

    def inputReject (label : A → K → Bool) (σ : K → Bool) (F : Cube A → Bool) : ℝ :=
…
  108. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.testerReject line 769
  109. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.andReject_nonneg line 772
  110. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.unitReject_nonneg line 785
  111. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.inputReject_nonneg line 791
  112. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.andReject_transfer line 799
  113. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.parity_zero line 823
  114. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.unitReject_zero_parity line 828
  115. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.parity_singleMask_eval line 841
  116. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.inputReject_transfer line 846
  117. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.tester_proximity_soundness line 865

    Source documentation

    Proximity soundness of the actual four finite tests. The only promise is the property being tested: the queried input is δ-far from every legal label.

    theorem tester_proximity_soundness (label : A → K → Bool) (σ : K → Bool)
    (F : Cube A → Bool) {δ : ℝ} (hδ : 0 < δ) (hδ' : δ ≤ 1 / 4)
    (hfar : ∀ a, δ ≤ distance σ (label a)) :
    δ / 256 ≤ testerReject label σ F := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AssignmentTester.distance, OAI.MaxCutGames.Foundations.PCP.AssignmentTester.testerReject

  118. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.selfCorrect_dictator line 913
  119. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.tester_perfect_completeness line 920

    Source documentation

    Every legal assignment has an honest proof accepted on every test.

    theorem tester_perfect_completeness (label : A → K → Bool) (a : A) :
    testerReject label (label a) (fun f => f a) = 0 := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AssignmentTester.testerReject

  120. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.eventQueries line 934

    Source documentation

    The actual six oracle addresses for each test. Unused slots repeat an address already queried, so every event has the same fixed six-slot format.

    def eventQueries (label : A → K → Bool) (kind : Fin 4) (k : K)
    (f g r₀ r₁ r₂ : Cube A) (slot : Fin 6) : K ⊕ Cube A :=
…
  121. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.eventAccepts line 950
  122. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.oracleAnswer line 956
  123. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.eventReject line 959
  124. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.truth_not_decide_eq line 964
  125. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.eventReject_blr line 968
  126. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.eventReject_and line 975
  127. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.eventReject_unit line 984
  128. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.eventReject_input line 995
  129. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.event_perfect_completeness line 1005

    Source documentation

    The honest proof satisfies each explicit event separately, including all padding slots, so it supplies actual satisfying labels in the incidence graph.

    theorem event_perfect_completeness (label : A → K → Bool) (a : A)
    (kind : Fin 4) (k : K) (f g r₀ r₁ r₂ : Cube A) :
    eventAccepts kind (fun slot => oracleAnswer (label a) (fun x => x a)
      (eventQueries label kind k f g r₀ r₁ r₂ slot)) = true := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AssignmentTester.eventAccepts, OAI.MaxCutGames.Foundations.PCP.AssignmentTester.oracleAnswer, OAI.MaxCutGames.Foundations.PCP.AssignmentTester.eventQueries

  130. def OAI.MaxCutGames.Foundations.PCP.AssignmentTester.explicitTesterReject line 1021

    Source documentation

    One finite uniform sample space for the executable six-address test.

    def explicitTesterReject (label : A → K → Bool) (σ : K → Bool) (F : Cube A → Bool) : ℝ :=
…
  131. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.explicitTesterReject_eq line 1025
  132. theorem OAI.MaxCutGames.Foundations.PCP.AssignmentTester.explicit_proximity_soundness line 1032