OAI/Computability/UniqueGames/Soundness/ConditionalLocality.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Complete local private inputs after fixing H

The constructors here consume only the appropriate zero-set question tuple: occurrences for the first player, names for the second. A single reference sample from the positive observation fibre is fixed once as part of H-dependent advice. It supplies arbitrary padding at hidden positions and never depends on the actual remaining sample. The reconstruction theorems prove equality of the complete question-plus-row input, and the row maps restrict to the actual equation spaces as shown in ZeroInformation.supplied_map_pullback.

  1. instance OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.zeroBits line 21
  2. def OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.membershipBool line 24
  3. def OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.fullCoefficient line 27
  4. def OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.singleCoefficient line 32
  5. def OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.fillHidden line 36
  6. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.singleCoefficient_zero line 40
  7. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.zeroSet_subset line 48
  8. def OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.actualFirst line 58
  9. def OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.actualSecond line 63
  10. def OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.localFirstFromH line 68
  11. def OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.localSecondFromH line 79
  12. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.localFirstFromH_question_inside line 91
  13. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.localSecondFromH_question_inside line 101
  14. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.outside_pair_agree line 113
  15. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.fillHidden_occurrences line 119
  16. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.fillHidden_names line 131
  17. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.localFirstFromH_correct line 143

    Source documentation

    Equality of the entire first private input, including its row map.

    theorem localFirstFromH_correct
    (distinct : ∀ o i i', name o i = name o i' → i = i')
    (reference sample : RawObservationFibre J name gamma observed) :
    localFirstFromH J name gamma observed reference (fun j => (sample.val.2 j.val).1) =
      actualFirst J gamma sample.val.2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.RawObservationFibre, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.localFirstFromH, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.actualFirst

  18. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.localSecondFromH_correct line 165

    Source documentation

    Equality of the entire second private input. The constructor requires no occurrence, equation rhs, or slot from any position in K.

    theorem localSecondFromH_correct (reference sample : RawObservationFibre J name gamma observed) :
    localSecondFromH J name gamma observed reference
        (fun j => name (sample.val.2 j.val).1 (sample.val.2 j.val).2) =
      actualSecond J name gamma sample.val.2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.RawObservationFibre, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.localSecondFromH, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.actualSecond