OAI/Computability/UniqueGames/PCP/AssignmentTester.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

A concrete constant-query proximity tester for a finite relation.

The proof oracle is a Boolean function on the Boolean functions on the finite set of legal assignments. The tests are BLR linearity, self-corrected AND, self-corrected unit, and comparison with a queried input coordinate. The oracle's size depends exponentially on the number of legal assignments; this is a fixed-relation construction, not a polynomial-size tester for an arbitrary input formula. All tests below are explicit finite expectations.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.truth line 28
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.disagree line 30
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.truth_nonneg line 32
  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.disagree_nonneg line 34
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.disagree_eq line 37
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.disagree_xor_le line 41
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.parity line 45
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.bitSign_parity line 48
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.bitSign_injective line 56
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.parity_xor line 60
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.cubeXor_comm line 66
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.cubeXor_right_twice line 71
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.expect_cubeXor line 77
  14. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.distance line 92
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.distance_nonneg line 95
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.distance_parity line 101
  17. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.blrReject line 109
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.blrReject_nonneg line 112
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.blr_correlation line 119
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.blrReject_fourier line 138
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.blr_near_parity line 148

    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.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.distance, OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.parity, OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.blrReject

  22. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.selfCorrect line 178
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.parity_selfCorrect line 181
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.selfCorrect_error line 187

    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.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.disagree, OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.selfCorrect, OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.parity, OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.distance

  25. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.singleMask line 201
  26. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.flipAt line 203
  27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.flipAt_twice line 207
  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.flipAt_eq_xor line 212
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.expect_flipAt line 216
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.walsh_singleMask line 221
  31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.parity_singleMask line 231
  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.parity_flipAt line 235
  33. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.cubeAnd line 240
  34. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.andLawFailure line 242
  35. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.andLawFailure_flipAt_second line 245
  36. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.four_truth_lower line 262
  37. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.parity_and_rejection line 268

    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.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.truth, OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.andLawFailure

  38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.truth_xor line 297
  39. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.disagree_triangle line 300
  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.and_disagree_transfer line 304
  41. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.andReject line 311

    Source documentation

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

    def andReject (F : Cube A → Bool) : ℝ :=
…
  42. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.unitReject line 316
  43. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.inputReject line 322

    Source documentation

    One original input query and two proof-oracle queries.

    def inputReject (label : A → K → Bool) (σ : K → Bool) (F : Cube A → Bool) : ℝ :=
…
  44. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.testerReject line 325
  45. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.andReject_nonneg line 328
  46. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.unitReject_nonneg line 341
  47. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.inputReject_nonneg line 347
  48. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.andReject_transfer line 355
  49. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.parity_zero line 379
  50. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.unitReject_zero_parity line 384
  51. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.parity_singleMask_eval line 397
  52. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.inputReject_transfer line 402
  53. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.tester_proximity_soundness line 421

    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.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.distance, OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.testerReject

  54. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.selfCorrect_dictator line 469
  55. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.tester_perfect_completeness line 476

    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.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.testerReject

  56. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.eventQueries line 490

    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 :=
…
  57. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.eventAccepts line 506
  58. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.oracleAnswer line 512
  59. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.eventReject line 515
  60. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.truth_not_decide_eq line 520
  61. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.eventReject_blr line 527
  62. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.eventReject_and line 533
  63. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.eventReject_unit line 541
  64. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.eventReject_input line 551
  65. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.event_perfect_completeness line 560

    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.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.eventAccepts, OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.oracleAnswer, OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.eventQueries

  66. def OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.explicitTesterReject line 578

    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) : ℝ :=
…
  67. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.explicitTesterReject_eq line 582
  68. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.explicit_proximity_soundness line 589