OAI/Computability/MaxCut/Model2.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite occurrence presentations used by the v2 rounding/subdivision construction. An occurrence has its own identifier: its endpoints need not be distinct and different occurrences may have the same endpoints. The bipartite target records injectivity of the pair of endpoints, which is precisely the required simplicity. No hardness or analytic premise enters these structures.

  1. structure OAI.MaxCutGames.Explicit.OccurrenceGame line 16
  2. structure OAI.MaxCutGames.Explicit.BipartiteGame line 21
  3. def OAI.MaxCutGames.Explicit.OccurrenceGame.Satisfied line 29
  4. instance OAI.MaxCutGames.Explicit.OccurrenceGame.satisfiedDecidable line 33
  5. def OAI.MaxCutGames.Explicit.OccurrenceGame.IsTranslation line 37
  6. def OAI.MaxCutGames.Explicit.BipartiteGame.Satisfied line 44
  7. instance OAI.MaxCutGames.Explicit.BipartiteGame.satisfiedDecidable line 48
  8. def OAI.MaxCutGames.Explicit.BipartiteGame.IsTranslation line 52