OAI/Computability/UniqueGames/PCP/PreprocessingOverlayTables.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.overlayPorts line 15

    Source documentation

    Old ports precede expander ports.

    def overlayPorts (d e : Nat) : (Fin d ⊕ Fin e) ≃ Fin (d + e) := finSumFinEquiv
  2. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.overlayPorts_inl_val line 17
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.overlayPorts_inr_val line 20
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.lazyPorts line 25

    Source documentation

    False/stay ports occupy rows 0,...,d-1; true/move ports occupy rows d,...,2*d-1, before the vertex offset is added.

    def lazyPorts (d : Nat) : (Bool × Fin d) ≃ Fin (2 * d) :=
…
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.lazyPorts_false_val line 28
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.lazyPorts_true_val line 32
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.materialize line 39

    Source documentation

    Materialize explicitly supplied pair-dart semantics in numbered port coordinates. The executable rotation only conjugates G.reverse by ports. The hypothesis about reversal affects proofs, not stored data.

    def materialize {n d : Nat} {D : Type*}
    (G : ConstraintGraph (Fin n) (Fin n × D) PortTables.Label)
    (ports : D ≃ Fin d) : PortTables.Table n d :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Label, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table

  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.rotation_materialize line 53
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.rotation_materialize_image line 64
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.accepts_materialize line 71
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.constraintGraph_ext line 78
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.baseGraph_materialize line 92
  13. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.overlay line 109

    Source documentation

    Add the expander's stored ports; every new constraint always accepts.

    def overlay {n d e : Nat} (G : PortTables.Table n d) (H : ExpanderTables.Table n e) :
    PortTables.Table n (d + e) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table

  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.overlay_rotation_old line 114
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.overlay_rotation_expander line 121
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.overlay_accepts_old line 128
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.overlay_accepts_expander line 135
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.overlay_semantics line 141
  19. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.lazy line 149
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.lazy_rotation_false line 152
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.lazy_rotation_true line 158
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.lazy_accepts_false line 165
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.lazy_accepts_true line 171
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.lazy_semantics line 178