OAI/Computability/UniqueGames/Decoding/TableKeysGame.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Decoder.TableKeysGame.Question line 13
  2. abbrev OAI.UniqueGamesTheorem.Decoder.TableKeysGame.Map line 14
  3. abbrev OAI.UniqueGamesTheorem.Decoder.TableKeysGame.Dual line 15
  4. abbrev OAI.UniqueGamesTheorem.Decoder.TableKeysGame.Query line 16
  5. abbrev OAI.UniqueGamesTheorem.Decoder.TableKeysGame.canonical line 17
  6. abbrev OAI.UniqueGamesTheorem.Decoder.TableKeysGame.Vertex line 20

    Source documentation

    One realized key orbit, with no prover-side copy.

    abbrev Vertex (S : Source) (k s d : Nat) := ActualGame.Vertex S k s d
  7. abbrev OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertex line 21
  8. abbrev OAI.UniqueGamesTheorem.Decoder.TableKeysGame.offset line 22
  9. abbrev OAI.UniqueGamesTheorem.Decoder.TableKeysGame.shiftQuery line 23
  10. def OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount line 25
  11. def OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexEncoding line 28
  12. abbrev OAI.UniqueGamesTheorem.Decoder.TableKeysGame.Outcome line 32

    Source documentation

    All four sampling choices remain separate occurrence indices.

    abbrev Outcome (S : Source) (k : Nat) {s d : Nat} (g : SplitGadget s d) :=
…
  13. abbrev OAI.UniqueGamesTheorem.Decoder.TableKeysGame.leftQuery line 35
  14. abbrev OAI.UniqueGamesTheorem.Decoder.TableKeysGame.rightQuery line 37
  15. def OAI.UniqueGamesTheorem.Decoder.TableKeysGame.edge line 40
  16. def OAI.UniqueGamesTheorem.Decoder.TableKeysGame.outcomes line 47
  17. def OAI.UniqueGamesTheorem.Decoder.TableKeysGame.outputInstance line 50
  18. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysGame.outputInstance_constraints_length line 62
  19. def OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexLabel line 67
  20. def OAI.UniqueGamesTheorem.Decoder.TableKeysGame.labelingOf line 72
  21. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexLabel_labelingOf line 77
  22. def OAI.UniqueGamesTheorem.Decoder.TableKeysGame.unfolded line 84

    Source documentation

    Restore the removed alphabet component of the affine intercept.

    noncomputable def unfolded (S : Source) (k s d : Nat)
    (labeling : Fin (vertexCount S k s d) → Fin (2^s))
    (q : Query S k s d) : Alphabet s :=
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.TableKeysGame.Query

  23. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysGame.unfolded_equivariant line 89
  24. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysGame.edge_satisfied_iff line 100
  25. def OAI.UniqueGamesTheorem.Decoder.TableKeysGame.acceptanceProbability line 114
  26. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysGame.acceptanceProbability_eq_test line 118
  27. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysGame.countSatisfied_map line 130
  28. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysGame.countSatisfied_eq_sum line 138
  29. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysGame.acceptanceProbability_eq_count line 147

    Source documentation

    The test probability is the satisfied fraction of the actual occurrence list.

    theorem acceptanceProbability_eq_count (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (labeling : Fin (vertexCount S k s d) → Fin (2^s)) :
    acceptanceProbability S k g labeling =
      (countSatisfied labeling (outputInstance S k g).constraints : ℚ) /
        (outputInstance S k g).constraints.length := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.TableKeysGame.acceptanceProbability, OAI.UniqueGamesTheorem.Decoder.TableKeysGame.outputInstance

  30. def OAI.UniqueGamesTheorem.Decoder.TableKeysGame.explicitVertexCount line 158

    Source documentation

    Exhaustive numbering of the same single-orbit vertex type.

    def explicitVertexCount (S : Source) (k s d : Nat) : Nat :=
…
  31. def OAI.UniqueGamesTheorem.Decoder.TableKeysGame.explicitVertexEncoding line 161
  32. def OAI.UniqueGamesTheorem.Decoder.TableKeysGame.semanticToExplicitVertices line 167
  33. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysGame.semanticToExplicitVertices_apply line 171
  34. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysGame.explicitVertexCount_eq line 177
  35. def OAI.UniqueGamesTheorem.Decoder.TableKeysGame.explicitEdge line 181
  36. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysGame.explicitEdge_eq_rename line 188
  37. def OAI.UniqueGamesTheorem.Decoder.TableKeysGame.outputInstanceWithEnumeration line 196

    Source documentation

    Executable finite output, still allowing loops and parallel occurrences.

    def outputInstanceWithEnumeration (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (en : NoiseEnumeration g) : Instance (2^s) where
…
  38. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysGame.outputInstanceWithEnumeration_length line 209
  39. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysGame.explicitConstraints_perm_renamed line 216
  40. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysGame.completeAt_outputInstanceWithEnumeration_iff line 225
  41. theorem OAI.UniqueGamesTheorem.Decoder.TableKeysGame.soundAt_outputInstanceWithEnumeration_iff line 233