OAI/Computability/MaxCut/PCP/InitialGraph.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

The initial finite constraint graph of an arbitrary concrete 3CNF formula. Clause and variable vertices use one eight-element alphabet. Variable labels are the canonical triples (bit, false, false); clause labels are arbitrary triples. Every incidence has two directed darts, including repeated names. A tautological dummy loop keeps the graph nonempty for empty formulas.

Name compaction precedes the public construction. The resulting vertex count is at most 4*m+1, and the dart count is exactly 6*m+1. Unsatisfiability gives an inverse-size gap, not a constant gap. No PCP theorem is assumed or claimed.

  1. abbrev OAI.MaxCutGames.Foundations.PCP.InitialGraph.Label line 22
  2. abbrev OAI.MaxCutGames.Foundations.PCP.InitialGraph.Vertex line 23
  3. abbrev OAI.MaxCutGames.Foundations.PCP.InitialGraph.Dart line 24
  4. instance OAI.MaxCutGames.Foundations.PCP.InitialGraph.slotFintype line 26
  5. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.card_slot line 30
  6. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.card_label line 31
  7. def OAI.MaxCutGames.Foundations.PCP.InitialGraph.variableVertex line 34
  8. def OAI.MaxCutGames.Foundations.PCP.InitialGraph.clauseVertex line 35
  9. def OAI.MaxCutGames.Foundations.PCP.InitialGraph.dummyVertex line 36
  10. def OAI.MaxCutGames.Foundations.PCP.InitialGraph.dummyDart line 37
  11. instance OAI.MaxCutGames.Foundations.PCP.InitialGraph.vertexNonempty line 39
  12. instance OAI.MaxCutGames.Foundations.PCP.InitialGraph.dartNonempty line 40
  13. def OAI.MaxCutGames.Foundations.PCP.InitialGraph.reverse line 42
  14. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.reverse_involutive line 46
  15. def OAI.MaxCutGames.Foundations.PCP.InitialGraph.reverseEquiv line 52
  16. def OAI.MaxCutGames.Foundations.PCP.InitialGraph.tail line 58
  17. def OAI.MaxCutGames.Foundations.PCP.InitialGraph.toClauseAnswer line 63
  18. def OAI.MaxCutGames.Foundations.PCP.InitialGraph.fromClauseAnswer line 64
  19. def OAI.MaxCutGames.Foundations.PCP.InitialGraph.variableLabel line 65
  20. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.to_fromClauseAnswer line 67
  21. def OAI.MaxCutGames.Foundations.PCP.InitialGraph.variableValid line 71
  22. def OAI.MaxCutGames.Foundations.PCP.InitialGraph.incidenceAccept line 74
  23. def OAI.MaxCutGames.Foundations.PCP.InitialGraph.predicate line 80
  24. def OAI.MaxCutGames.Foundations.PCP.InitialGraph.raw line 85
  25. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.raw_forward line 96
  26. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.incidenceAccept_true line 101
  27. def OAI.MaxCutGames.Foundations.PCP.InitialGraph.honestLabeling line 108
  28. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.incidence_honest line 113
  29. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.raw_completeness line 121
  30. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.clauseAnswer_eq_of_slots line 130
  31. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.raw_reflects line 139
  32. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.raw_satisfiable_iff line 158
  33. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.card_vertex line 161
  34. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.card_dart line 165
  35. abbrev OAI.MaxCutGames.Foundations.PCP.InitialGraph.CompactVertex line 170
  36. abbrev OAI.MaxCutGames.Foundations.PCP.InitialGraph.CompactDart line 171
  37. def OAI.MaxCutGames.Foundations.PCP.InitialGraph.build line 173
  38. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.build_satisfiable_iff line 176
  39. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.build_vertex_bound line 180
  40. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.build_dart_count line 186
  41. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.build_initial_gap line 192

    Source documentation

    The initial inverse-size gap follows from the original unsatisfiability, without a PCP, bounded-degree, or constant-gap premise.

    theorem build_initial_gap (F : Formula) (unsat : ¬ F.Satisfiable)
    (labeling : CompactVertex F → Label) : 1 ≤ (build F).rejectionCount labeling := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.InitialGraph.CompactVertex, OAI.MaxCutGames.Foundations.PCP.InitialGraph.Label, OAI.MaxCutGames.Foundations.PCP.InitialGraph.build

  42. theorem OAI.MaxCutGames.Foundations.PCP.InitialGraph.build_inverse_size_gap line 198