OAI/Computability/MaxCut/PCP/HonestTest.lean

GitHub source file

81 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.MaxCutGames.Foundations.Hastad.dictator_test_parity line 24

    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.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.thirdQuery

  2. theorem OAI.MaxCutGames.Foundations.Hastad.noise_coordinate_sign line 31

    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.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.noiseWeight, OAI.MaxCutGames.Foundations.Hastad.bitSign

  3. theorem OAI.MaxCutGames.Foundations.Hastad.noise_coordinate_false line 42

    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.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.noiseWeight

  4. theorem OAI.MaxCutGames.Foundations.Hastad.testAcceptance_dictator line 56

    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.MaxCutGames.Foundations.Hastad.testAcceptance

  5. theorem OAI.MaxCutGames.Foundations.Hastad.testAcceptance_folded_dictators line 76

    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.MaxCutGames.Foundations.Hastad.testAcceptance, OAI.MaxCutGames.Foundations.Hastad.foldedAnswer

  6. theorem OAI.MaxCutGames.Foundations.Hastad.testAcceptance_conditioned_dictators line 89

    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.MaxCutGames.Foundations.Hastad.testAcceptance, OAI.MaxCutGames.Foundations.Hastad.conditionedFoldedAnswer

  7. theorem OAI.MaxCutGames.Foundations.Hastad.testAcceptance_folded_conditioned_dictators line 105
  8. def OAI.MaxCutGames.Foundations.Hastad.realizedTestAcceptance line 119

    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.MaxCutGames.Foundations.Hastad.Cube

  9. theorem OAI.MaxCutGames.Foundations.Hastad.realizedTestAcceptance_eq_testAcceptance line 126

    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.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.realizedTestAcceptance, OAI.MaxCutGames.Foundations.Hastad.testAcceptance

  10. theorem OAI.MaxCutGames.Foundations.Hastad.realizedTestAcceptance_dictator line 136

    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.MaxCutGames.Foundations.Hastad.realizedTestAcceptance

  11. theorem OAI.MaxCutGames.Foundations.Hastad.realizedTestAcceptance_folded_dictators line 142
  12. theorem OAI.MaxCutGames.Foundations.Hastad.realizedTestAcceptance_conditioned_dictators line 149
  13. theorem OAI.MaxCutGames.Foundations.Hastad.realizedTestAcceptance_folded_conditioned_dictators line 159
  14. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceTape.TestTape line 175

    Source documentation

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

    abbrev TestTape (I J : Type*) (D : ℕ) :=
…
  15. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceTape.FairTestTape line 178
  16. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.expect_prod line 184
  17. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.card_testTape line 195
  18. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.card_fairTestTape line 200
  19. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.expect_testTape line 206
  20. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.expect_equivTape line 215

    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.MaxCutGames.Foundations.Hastad.SourceTape.TestTape

  21. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.expect_fairTestTape line 220
  22. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.expect_fairTestTape_ignore line 229
  23. def OAI.MaxCutGames.Foundations.Hastad.SourceTape.tapeQueries line 235

    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.MaxCutGames.Foundations.Hastad.SourceTape.TestTape, OAI.MaxCutGames.Foundations.Hastad.Cube

  24. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.expect_tapeQueries line 239

    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.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.SourceTape.TestTape, OAI.MaxCutGames.Foundations.Hastad.SourceTape.tapeQueries, OAI.MaxCutGames.Foundations.Hastad.noiseWeight, OAI.MaxCutGames.Foundations.Hastad.thirdQuery

  25. def OAI.MaxCutGames.Foundations.Hastad.SourceTape.tapeAcceptance line 250
  26. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_realizedTestAcceptance line 256
  27. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_testAcceptance line 261
  28. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_sum_div_card line 267
  29. def OAI.MaxCutGames.Foundations.Hastad.SourceTape.restrictFunction line 279
  30. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.expect_restrictFunction line 284

    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.MaxCutGames.Foundations.Hastad.SourceTape.restrictFunction

  31. def OAI.MaxCutGames.Foundations.Hastad.SourceTape.restrictTape line 299
  32. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.expect_restrictTape line 303
  33. def OAI.MaxCutGames.Foundations.Hastad.SourceTape.restrictedProjection line 331
  34. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.restrict_realizedNoise line 335
  35. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.restrict_thirdQuery line 338
  36. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.expect_restricted_queries line 346

    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.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.SourceTape.TestTape, OAI.MaxCutGames.Foundations.Hastad.SourceTape.restrictFunction, OAI.MaxCutGames.Foundations.Hastad.thirdQuery, OAI.MaxCutGames.Foundations.Hastad.SourceTape.tapeQueries, OAI.MaxCutGames.Foundations.Hastad.SourceTape.restrictedProjection

  37. def OAI.MaxCutGames.Foundations.Hastad.SourceTape.restrictRightTape line 358
  38. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.expect_restrictRightTape line 362
  39. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTape.expect_rightRestricted_queries line 383

    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.MaxCutGames.Foundations.Hastad.Cube, OAI.MaxCutGames.Foundations.Hastad.SourceTape.TestTape, OAI.MaxCutGames.Foundations.Hastad.SourceTape.restrictFunction, OAI.MaxCutGames.Foundations.Hastad.thirdQuery, OAI.MaxCutGames.Foundations.Hastad.SourceTape.tapeQueries

  40. def OAI.MaxCutGames.Foundations.Hastad.SourceContexts.clauseAnswerEquiv line 404

    Source documentation

    Executable tuple encoding of the eight clause answers.

    def clauseAnswerEquiv : ClauseAnswer ≃ Bool × Bool × Bool where
…
  41. def OAI.MaxCutGames.Foundations.Hastad.SourceContexts.clauseAnswerFinEquiv line 410
  42. instance OAI.MaxCutGames.Foundations.Hastad.SourceContexts.clauseAnswerFintype line 416
  43. instance OAI.MaxCutGames.Foundations.Hastad.SourceContexts.clauseAnswerInhabited line 419
  44. instance OAI.MaxCutGames.Foundations.Hastad.SourceContexts.slotFintype line 421
  45. instance OAI.MaxCutGames.Foundations.Hastad.SourceContexts.slotInhabited line 425
  46. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.card_clauseAnswer line 427
  47. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.card_slot line 431
  48. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceContexts.I line 433
  49. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceContexts.J line 434
  50. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceContexts.ClauseContext line 435
  51. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceContexts.VariableContext line 436
  52. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceContexts.SlotContext line 437
  53. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.card_I line 439
  54. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.card_J line 440
  55. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.card_ClauseContext line 441
  56. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.card_VariableContext line 443
  57. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.card_SlotContext line 445
  58. def OAI.MaxCutGames.Foundations.Hastad.SourceContexts.localConsistent line 448
  59. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.localConsistent_eq_true_iff line 452
  60. def OAI.MaxCutGames.Foundations.Hastad.SourceContexts.validJ line 460

    Source documentation

    Satisfaction and consistency over all 3*u occurrence slots.

    def validJ (F : Formula) {u : ℕ} (c : ClauseContext F u) (j : J u) : Bool :=
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceContexts.ClauseContext, OAI.MaxCutGames.Foundations.Hastad.SourceContexts.J

  61. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.validJ_eq_true_iff line 465
  62. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.validJ_satisfies line 473
  63. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.validJ_consistent line 478
  64. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.validJ_localConsistent line 485
  65. def OAI.MaxCutGames.Foundations.Hastad.SourceContexts.canonicalSlot line 494

    Source documentation

    First matching visible occurrence, with the third slot as an off-support default. Its inputs contain no hidden incidence choice.

    def canonicalSlot {n : ℕ} (clause : Clause n) (v : Fin n) : Slot :=
…
  66. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.canonicalSlot_name line 498
  67. def OAI.MaxCutGames.Foundations.Hastad.SourceContexts.pi line 510
  68. def OAI.MaxCutGames.Foundations.Hastad.SourceContexts.sampledVariables line 514
  69. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.sampledVariables_supported line 518
  70. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.sampled_eq_pi line 523
  71. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.sampled_answers_eq_of_visible_eq line 533

    Source documentation

    Two hidden choices with the same visible variable tuple give the same selected answers for every valid label.

    theorem sampled_answers_eq_of_visible_eq (F : Formula) {u : ℕ}
    (c : ClauseContext F u) (s s' : SlotContext u) (j : J u)
    (hj : validJ F c j = true)
    (hvisible : sampledVariables F c s = sampledVariables F c s') :
    (fun t => answerAt (j t) (s t)) = fun t => answerAt (j t) (s' t) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceContexts.ClauseContext, OAI.MaxCutGames.Foundations.Hastad.SourceContexts.SlotContext, OAI.MaxCutGames.Foundations.Hastad.SourceContexts.J, OAI.MaxCutGames.Foundations.Hastad.SourceContexts.validJ, OAI.MaxCutGames.Foundations.Hastad.SourceContexts.sampledVariables

  72. def OAI.MaxCutGames.Foundations.Hastad.SourceContexts.honestJ line 541
  73. def OAI.MaxCutGames.Foundations.Hastad.SourceContexts.honestI line 545
  74. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.honestJ_valid line 549
  75. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.pi_honest line 561
  76. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.pi_honest_sampled line 569
  77. def OAI.MaxCutGames.Foundations.Hastad.SourceContexts.baseAccepts line 575
  78. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.baseAccepts_eq_true_iff line 581
  79. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.projection_implies_coordinate_accepts line 589
  80. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.baseAccepts_implies_sampled line 596
  81. theorem OAI.MaxCutGames.Foundations.Hastad.SourceContexts.projection_implies_sampled_accepts line 608

    Source documentation

    Every coordinate of the original repeated clause-slot verifier accepts the decoded answers. Each answer tuple may depend on its whole private context.

    theorem projection_implies_sampled_accepts (F : Formula) {u : ℕ}
    (c : ClauseContext F u) (s : SlotContext u) (i : I u) (j : J u)
    (hj : validJ F c j = true) (hpi : pi F c (sampledVariables F c s) j = i) :
    ∀ t, (localSatisfies (clauseAt F (c t)) (j t) &&
      decide (answerAt (j t) (s t) = i t)) = true := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceContexts.ClauseContext, OAI.MaxCutGames.Foundations.Hastad.SourceContexts.SlotContext, OAI.MaxCutGames.Foundations.Hastad.SourceContexts.I, OAI.MaxCutGames.Foundations.Hastad.SourceContexts.J, OAI.MaxCutGames.Foundations.Hastad.SourceContexts.validJ, OAI.MaxCutGames.Foundations.Hastad.SourceContexts.pi, OAI.MaxCutGames.Foundations.Hastad.SourceContexts.sampledVariables