OAI/Computability/MaxCut/Games/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.MaxCutGames.Soundness.RawPrivateTable.Extension line 20
  2. def OAI.MaxCutGames.Soundness.RawPrivateTable.displayed line 22
  3. theorem OAI.MaxCutGames.Soundness.RawPrivateTable.full_occurrence_eq_of_displayed_eq line 28
  4. theorem OAI.MaxCutGames.Soundness.RawPrivateTable.single_name_eq_of_displayed_eq line 35
  5. theorem OAI.MaxCutGames.Soundness.RawPrivateTable.displayed_eq_iff line 44
  6. def OAI.MaxCutGames.Soundness.RawPrivateTable.SupportedV line 60
  7. def OAI.MaxCutGames.Soundness.RawPrivateTable.representative line 64
  8. theorem OAI.MaxCutGames.Soundness.RawPrivateTable.representative_display line 67
  9. def OAI.MaxCutGames.Soundness.RawPrivateTable.supported line 72
  10. def OAI.MaxCutGames.Soundness.RawPrivateTable.projection line 81
  11. def OAI.MaxCutGames.Soundness.RawPrivateTable.merge line 85
  12. theorem OAI.MaxCutGames.Soundness.RawPrivateTable.merge_comp line 90
  13. def OAI.MaxCutGames.Soundness.RawPrivateTable.sourceTable line 95
  14. def OAI.MaxCutGames.Soundness.RawPrivateTable.privateTable line 100
  15. theorem OAI.MaxCutGames.Soundness.RawPrivateTable.canonical_same_display line 107
  16. theorem OAI.MaxCutGames.Soundness.RawPrivateTable.privateTable_pullback line 120

    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.MaxCutGames.Soundness.RawPrivateTable.privateTable, OAI.MaxCutGames.Soundness.RawPrivateTable.supported, OAI.MaxCutGames.Soundness.RawPrivateTable.sourceTable, OAI.MaxCutGames.Soundness.RawPrivateTable.projection