OAI/Computability/UniqueGames/Soundness/RawPrivateTable.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The private Fourier table is defined from displayed data alone. Compatibility with every hidden extension follows from the proved canonical locality theorem.

  1. abbrev OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.Extension line 21
  2. def OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.displayed line 23
  3. theorem OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.full_occurrence_eq_of_displayed_eq line 29
  4. theorem OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.single_name_eq_of_displayed_eq line 36
  5. theorem OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.displayed_eq_iff line 45
  6. def OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.SupportedV line 61
  7. def OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.representative line 65
  8. theorem OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.representative_display line 68
  9. def OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.supported line 73
  10. def OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.projection line 82
  11. def OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.merge line 86
  12. theorem OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.merge_comp line 91
  13. def OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.sourceTable line 96
  14. def OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.privateTable line 101
  15. theorem OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.canonical_same_display line 108
  16. theorem OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.privateTable_pullback line 121

    Source documentation

    Exact table compatibility with no extension or hidden question supplied to the private table. The row and column are merged before canonicalization.

    theorem privateTable_pullback (split : R ≃ₗ[F2] D × C)
    (label : ActualCanonical.Data k Name Id R → Label)
    (occ : Fin k → Id) (slot : Fin k → Slot)
    (Z : RawPoint J →ₗ[F2] D) (X : RawPoint J →ₗ[F2] C) :
    privateTable J names rhs split label (supported J names occ slot) Z X =
      sourceTable names rhs split label occ
        (Z.comp (projection J rhs occ slot)) (X.comp (projection J rhs occ slot)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.privateTable, OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.supported, OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.sourceTable, OAI.UniqueGamesTheorem.Soundness.RawPrivateTable.projection