OAI/Computability/UniqueGames/PCP/HonestTestLemmas.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Honest completeness of the actual three-query test. Compatible coordinate dictators cancel the two uniform query tables, leaving exactly one noise bit. The finite-tape form uses the proved product-noise pushforward law.

  1. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.dictator_test_parity line 28

    Source documentation

    For compatible honest coordinates, the test parity is precisely the selected noise coordinate, for every individual choice of query tables.

    theorem dictator_test_parity (π : J → I) (i : I) (j : J) (hπ : π j = i)
    (f : Cube I) (g μ : Cube J) :
    (f i ^^ g j ^^ (thirdQuery π f g μ) j) = μ j := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.thirdQuery

  2. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.noise_coordinate_sign line 35

    Source documentation

    The product noise law has the specified sign bias in every coordinate.

    theorem noise_coordinate_sign (ε : ℝ) (j : J) :
    (∑ μ : Cube J, noiseWeight ε μ * bitSign (μ j)) = 1 - 2 * ε := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.noiseWeight, OAI.UniqueGamesTheorem.Foundations.Hastad.bitSign

  3. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.noise_coordinate_false line 46

    Source documentation

    The probability of a false noise bit is exactly 1 - ε. This is an algebraic identity of the explicit product weights, valid for every real ε.

    theorem noise_coordinate_false (ε : ℝ) (j : J) :
    (∑ μ : Cube J, noiseWeight ε μ * if μ j then (0 : ℝ) else 1) = 1 - ε := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.noiseWeight

  4. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.testAcceptance_dictator line 60

    Source documentation

    Exact honest acceptance for the actual three-bit test.

    theorem testAcceptance_dictator (ε : ℝ) (π : J → I)
    (i : I) (j : J) (hπ : π j = i) :
    testAcceptance ε π (fun f => f i) (fun g => g j) = 1 - ε := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.testAcceptance

  5. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.testAcceptance_folded_dictators line 80

    Source documentation

    Storing an honest dictator in the actual half-table representation gives the same acceptance after applying the explicit folding correction.

    theorem testAcceptance_folded_dictators (ε : ℝ) (π : J → I)
    (i₀ i : I) (j₀ j : J) (hπ : π j = i) :
    testAcceptance ε π (foldedAnswer i₀ (fun h => h.val i))
      (foldedAnswer j₀ (fun h => h.val j)) = 1 - ε := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.testAcceptance, OAI.UniqueGamesTheorem.Foundations.Hastad.foldedAnswer

  6. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.testAcceptance_conditioned_dictators line 93

    Source documentation

    Honest valid local assignments remain dictators after both conditioning and folding, so the concrete conditioned tables have the same completeness.

    theorem testAcceptance_conditioned_dictators (ε : ℝ) (π : J → I)
    (validI : I → Bool) (validJ : J → Bool)
    (i₀ i : {i : I // validI i = true}) (j₀ j : {j : J // validJ j = true})
    (hπ : π j.val = i.val) :
    testAcceptance ε π
      (conditionedFoldedAnswer validI i₀ (fun h => h.val i))
      (conditionedFoldedAnswer validJ j₀ (fun h => h.val j)) = 1 - ε := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.testAcceptance, OAI.UniqueGamesTheorem.Foundations.Hastad.conditionedFoldedAnswer

  7. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.testAcceptance_folded_conditioned_dictators line 109
  8. def OAI.UniqueGamesTheorem.Foundations.Hastad.realizedTestAcceptance line 123

    Source documentation

    The actual test using one uniform Fin D tape entry per noise coordinate.

    def realizedTestAcceptance (D : Nat) (π : J → I)
    (A : Cube I → Bool) (B : Cube J → Bool) : ℝ :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube

  9. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.realizedTestAcceptance_eq_testAcceptance line 130

    Source documentation

    Exact equality between the finite uniform tape and the weighted product noise test; no distributional acceptance premise is assumed.

    theorem realizedTestAcceptance_eq_testAcceptance {D : Nat} (positive : 0 < D)
    (π : J → I) (A : Cube I → Bool) (B : Cube J → Bool) :
    realizedTestAcceptance D π A B = testAcceptance ((D : ℝ)⁻¹) π A B := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.realizedTestAcceptance, OAI.UniqueGamesTheorem.Foundations.Hastad.testAcceptance

  10. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.realizedTestAcceptance_dictator line 140

    Source documentation

    Exact honest completeness of the uniformly sampled finite-tape test.

    theorem realizedTestAcceptance_dictator {D : Nat} (positive : 0 < D)
    (π : J → I) (i : I) (j : J) (hπ : π j = i) :
    realizedTestAcceptance D π (fun f => f i) (fun g => g j) = 1 - (D : ℝ)⁻¹ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.realizedTestAcceptance

  11. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.realizedTestAcceptance_folded_dictators line 146
  12. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.realizedTestAcceptance_conditioned_dictators line 153
  13. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.realizedTestAcceptance_folded_conditioned_dictators line 163
  14. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.TestTape line 187

    Source documentation

    Two full Boolean query tables and one finite noise entry per right index.

    abbrev TestTape (I J : Type*) (D : ℕ) :=
…
  15. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.FairTestTape line 190
  16. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.expect_prod line 196
  17. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.card_testTape line 207
  18. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.card_fairTestTape line 212
  19. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.expect_testTape line 218
  20. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.expect_equivTape line 227

    Source documentation

    Any explicit finite enumeration equivalence preserves the exact tape law.

    theorem expect_equivTape {E : Type*} [Fintype E]
    (e : E ≃ TestTape I J D) (H : TestTape I J D → ℝ) :
    (𝔼 s : E, H (e s)) = 𝔼 t : TestTape I J D, H t :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.TestTape

  21. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.expect_fairTestTape line 232
  22. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.expect_fairTestTape_ignore line 241
  23. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.tapeQueries line 247

    Source documentation

    The three actual query tables read from a uniform finite tape.

    def tapeQueries (π : J → I) (t : TestTape I J D) : Cube I × Cube J × Cube J :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.TestTape, OAI.UniqueGamesTheorem.Foundations.Hastad.Cube

  24. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.expect_tapeQueries line 251

    Source documentation

    Exact joint law of all three queries, for every real-valued observable.

    theorem expect_tapeQueries (positive : 0 < D) (π : J → I)
    (H : Cube I × Cube J × Cube J → ℝ) :
    (𝔼 t : TestTape I J D, H (tapeQueries π t)) =
      𝔼 f : Cube I, ∑ μ : Cube J, noiseWeight ((D : ℝ)⁻¹) μ *
        (𝔼 g : Cube J, H (f, g, thirdQuery π f g μ)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.TestTape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.tapeQueries, OAI.UniqueGamesTheorem.Foundations.Hastad.noiseWeight, OAI.UniqueGamesTheorem.Foundations.Hastad.thirdQuery

  25. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.tapeAcceptance line 262
  26. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.tapeAcceptance_eq_realizedTestAcceptance line 268
  27. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.tapeAcceptance_eq_testAcceptance line 273
  28. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.tapeAcceptance_eq_sum_div_card line 279
  29. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.restrictFunction line 293
  30. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.expect_restrictFunction line 298

    Source documentation

    Uniform full functions push forward to uniform functions on any subtype. Nonempty values ensure that the unused coordinates can be filled.

    theorem expect_restrictFunction [Fintype X] [DecidableEq X] [Fintype Λ] [Nonempty Λ]
    (P : X → Prop) [DecidablePred P] (H : ({x : X // P x} → Λ) → ℝ) :
    (𝔼 f : X → Λ, H (restrictFunction P f)) =
      𝔼 g : {x : X // P x} → Λ, H g := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.restrictFunction

  31. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.restrictTape line 313
  32. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.expect_restrictTape line 317
  33. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.restrictedProjection line 345
  34. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.restrict_realizedNoise line 349
  35. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.restrict_thirdQuery line 352
  36. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.expect_restricted_queries line 360

    Source documentation

    The contextual three-query law is the same joint law as sampling directly on the contextual domains, whenever the contextual projection is defined.

    theorem expect_restricted_queries [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J]
    (P : I → Prop) (Q : J → Prop) [DecidablePred P] [DecidablePred Q]
    (π : J → I) (hπ : ∀ j, Q j → P (π j)) {D : ℕ} (positive : 0 < D)
    (H : Cube {i : I // P i} × Cube {j : J // Q j} × Cube {j : J // Q j} → ℝ) :
    (𝔼 t : TestTape I J D,
      H (restrictFunction P t.1, restrictFunction Q t.2.2,
        restrictFunction Q (thirdQuery π t.1 t.2.2 (realizedNoise t.2.1)))) =
    𝔼 t : TestTape {i : I // P i} {j : J // Q j} D,
      H (tapeQueries (restrictedProjection P Q π hπ) t) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.TestTape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.restrictFunction, OAI.UniqueGamesTheorem.Foundations.Hastad.thirdQuery, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.tapeQueries, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.restrictedProjection

  37. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.restrictRightTape line 372
  38. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.expect_restrictRightTape line 376
  39. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.expect_rightRestricted_queries line 397

    Source documentation

    Joint contextual law with the full left domain unchanged. No compatibility premise is needed: the right projection is simply restricted to valid indices.

    theorem expect_rightRestricted_queries [Fintype I] [DecidableEq I]
    [Fintype J] [DecidableEq J] (Q : J → Prop) [DecidablePred Q]
    (π : J → I) {D : ℕ} (positive : 0 < D)
    (H : Cube I × Cube {j : J // Q j} × Cube {j : J // Q j} → ℝ) :
    (𝔼 t : TestTape I J D,
      H (t.1, restrictFunction Q t.2.2,
        restrictFunction Q (thirdQuery π t.1 t.2.2 (realizedNoise t.2.1)))) =
    𝔼 t : TestTape I {j : J // Q j} D,
      H (tapeQueries (fun j => π j.val) t) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.Cube, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.TestTape, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.restrictFunction, OAI.UniqueGamesTheorem.Foundations.Hastad.thirdQuery, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTape.tapeQueries

  40. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.event_nonempty line 425
  41. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.eventLaw line 429
  42. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.visibleQuestion line 434
  43. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.baseGame line 438
  44. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.baseGame_accepts line 443
  45. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.eventLaw_probability line 447
  46. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.sum_slots line 460
  47. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.sum_slot_accepts line 470
  48. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.failureCount_eq_sum_map line 484
  49. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.failureCount_allIndices line 492
  50. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.verifier_probability_plus_failure line 501

    Source documentation

    The local three-slot rejection inequality controls the actual uniform incidence law, including repeated variable names and repeated clauses.

    theorem verifier_probability_plus_failure (F : Formula) (hne : F.clauses ≠ [])
    (alice : AliceStrategy F) (bob : BobStrategy F) :
    (eventLaw F hne).probability (accepts F alice bob) +
      (failureCount F bob (allIndices F) : ℝ) / (3 * F.clauses.length : ℕ) ≤ 1 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.eventLaw

  51. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.base_success_le_verifier line 522
  52. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.base_value_le_of_clause_gap line 533

    Source documentation

    A concrete clause-count gap supplies the base-game value bound.

    theorem base_value_le_of_clause_gap (F : Formula) (hne : F.clauses ≠ [])
    (δ : ℝ) (hgap : ∀ bob : BobStrategy F,
      δ * F.clauses.length ≤ (failureCount F bob (allIndices F) : ℝ)) :
    (baseGame F hne).value ≤ 1 - δ / 3 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.baseGame

  53. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.pushforward_comp line 553
  54. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.expectation_pushforward line 568
  55. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.repeatedVisible line 579
  56. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.repeated_questions line 586

    Source documentation

    This identifies the repeated game law with the actual uniformly sampled incidence tuples, retaining all collisions of their visible questions.

    theorem repeated_questions (F : Formula) (hne : F.clauses ≠ []) (u : ℕ) :
    ((baseGame F hne).repetition u).questions =
      ((eventLaw F hne).iid u).pushforward (repeatedVisible F u) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.baseGame, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.eventLaw, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.repeatedVisible

  57. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.repeated_expectation line 595
  58. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.repeated_expectation_split line 608

    Source documentation

    The concrete constructor enumerates clause tuples and slot tuples as separate lexicographic factors; this is exactly the same question law.

    theorem repeated_expectation_split (F : Formula) (hne : F.clauses ≠ []) (u : ℕ)
    (H : VariableContext F u × ClauseContext F u → ℝ) :
    ((baseGame F hne).repetition u).questions.expectation H =
      𝔼 c : ClauseContext F u, 𝔼 s : SlotContext u,
        H (sampledVariables F c s, c) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.baseGame

  59. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.sourceProjectionGame line 622
  60. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.projection_value_le_repetition line 629

    Source documentation

    The projection game has exactly the repeated question law, and its legal right answers satisfy every coordinate of the original game.

    theorem projection_value_le_repetition (F : Formula) (hne : F.clauses ≠ [])
    (u : ℕ) :
    (sourceProjectionGame F hne u).value ≤ ((baseGame F hne).repetition u).value := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.sourceProjectionGame, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.baseGame

  61. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.source_acceptance_le line 648
  62. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceGame.source_acceptance_le_split line 663