OAI/Computability/UniqueGames/Soundness/ActualPointAnswers.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Conversion of actual binary linear points to the named projection answers.

  1. def OAI.UniqueGamesTheorem.Soundness.ActualPointAnswers.sourceTau line 21
  2. def OAI.UniqueGamesTheorem.Soundness.ActualPointAnswers.partnerTau line 22
  3. theorem OAI.UniqueGamesTheorem.Soundness.ActualPointAnswers.tau_projection line 24
  4. def OAI.UniqueGamesTheorem.Soundness.ActualPointAnswers.firstAnswer line 31
  5. def OAI.UniqueGamesTheorem.Soundness.ActualPointAnswers.secondAnswer line 36
  6. theorem OAI.UniqueGamesTheorem.Soundness.ActualPointAnswers.triple_eq_of_first_second_parity line 41
  7. theorem OAI.UniqueGamesTheorem.Soundness.ActualPointAnswers.secondAnswer_projection line 58

    Source documentation

    Inactive occurrences determine every full triple. The active right-hand sides never enter the partner answer.

    theorem secondAnswer_projection (rhs rhs' : Fin k → Bool) (J : Finset (Fin k))
    (slot : Fin k → Slot) (x : ActualHomogeneous.E k)
    (hout : ∀ j, j ∉ J → rhs' j = rhs j) :
    secondAnswer rhs' J (rawProjection rhs J slot x) =
      ActualProjection.project (activeOf J) (fun j => ConcreteExtraction.slotIndex (slot j))
        (firstAnswer rhs x) := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.ActualPointAnswers.secondAnswer, OAI.UniqueGamesTheorem.Soundness.ConcreteExtraction.slotIndex, OAI.UniqueGamesTheorem.Soundness.ActualPointAnswers.firstAnswer

  8. def OAI.UniqueGamesTheorem.Soundness.ActualPointAnswers.displayedRhs line 108
  9. theorem OAI.UniqueGamesTheorem.Soundness.ActualPointAnswers.displayedRhs_full line 113
  10. theorem OAI.UniqueGamesTheorem.Soundness.ActualPointAnswers.actual_accepts line 121

    Source documentation

    Actual point equality gives acceptance in the named verifier on complete private inputs, with local answer conversions.

    theorem actual_accepts {Q Id Name : Type} (J : Finset (Fin k))
    (g : IncidenceExtraction.Incidence Id Name)
    (qa : ZeroInformation.FirstInput (Fin k) Q Id)
    (qb : ZeroInformation.SecondInput (Fin k) Q Id Name)
    (slot : Fin k → Slot)
    (hquestion : qb.question = RawPrivateTable.displayed J g.name qa.question slot)
    (x : ActualHomogeneous.E k) (v : RawPoint J)
    (hone : sourceTau x = 1)
    (hprojection : rawProjection (fun j => g.rhs (qa.question j)) J slot x = v) :
    ActualProjection.accepts g (activeOf J) qa qb
      (firstAnswer (fun j => g.rhs (qa.question j)) x)
      (secondAnswer (displayedRhs g.rhs qb.question) J v) := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.IncidenceExtraction.Incidence, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.FirstInput, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.SecondInput, OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.displayed, OAI.UniqueGamesTheorem.Soundness.ActualPointAnswers.sourceTau, OAI.UniqueGamesTheorem.Soundness.ActualPointAnswers.firstAnswer, OAI.UniqueGamesTheorem.Soundness.ActualPointAnswers.secondAnswer, OAI.UniqueGamesTheorem.Soundness.ActualPointAnswers.displayedRhs