OAI/Computability/MaxCut/PCP/GraphGap.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

Actual finite counting for rounding copied dart labels. Minority color classes are small enough for the cloud's directed-cut expansion. Their boundary darts inject into all label disagreements. A separate endpoint charge counts at most two affected original darts per changed copied label.

  1. def OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.rejectionCounts line 17
  2. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.rejectionCounts_nonempty line 21
  3. def OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.minimumRejections line 26
  4. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.minimumRejections_le line 29
  5. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.exists_minimizer line 34
  6. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.le_minimumRejections_iff line 41
  7. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.minimumRejections_le_card line 51
  8. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.rejectionCount_eq_zero_iff line 58
  9. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.minimumRejections_eq_zero_iff line 73
  10. def OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.gap line 83
  11. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.gap_nonnegative line 86
  12. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.gap_le_one line 89
  13. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.gap_eq_zero_iff line 95
  14. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.le_gap_iff line 102

    Source documentation

    A lower bound on the actual minimum is exactly the universal count bound.

    theorem le_gap_iff [Nonempty E] (G : ConstraintGraph V E A) (ε : ℝ) :
    ε ≤ G.gap ↔ ∀ labeling : V → A,
      ε * Fintype.card E ≤ (G.rejectionCount labeling : ℝ) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph

  15. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.inverse_card_le_gap_of_unsatisfiable line 115
  16. def OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.reindex line 130

    Source documentation

    Explicit changes of vertex, dart, and label coordinates.

    def reindex (G : ConstraintGraph V E A) (vertices : V ≃ W) (darts : E ≃ D)
    (labels : A ≃ B) : ConstraintGraph W D B where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph

  17. def OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.labelingEquiv line 144
  18. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.reindex_edgeSatisfied line 150
  19. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.reindex_rejectionCount line 157
  20. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.rejectionCounts_reindex line 181
  21. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.minimumRejections_reindex line 198
  22. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.gap_reindex line 204
  23. theorem OAI.MaxCutGames.Foundations.PCP.ConstraintGraph.satisfiable_reindex line 210
  24. def OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.overlayPorts line 225

    Source documentation

    Old ports precede expander ports.

    def overlayPorts (d e : Nat) : (Fin d ⊕ Fin e) ≃ Fin (d + e) := finSumFinEquiv
  25. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.overlayPorts_inl_val line 227
  26. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.overlayPorts_inr_val line 230
  27. def OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.lazyPorts line 235

    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) :=
…
  28. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.lazyPorts_false_val line 238
  29. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.lazyPorts_true_val line 242
  30. def OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.materialize line 249

    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.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.PortTables.Label, OAI.MaxCutGames.Foundations.PCP.PortTables.Table

  31. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.rotation_materialize line 262
  32. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.rotation_materialize_image line 273
  33. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.accepts_materialize line 280
  34. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.constraintGraph_ext_inline_PreprocessingOverlayTables line 287
  35. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.baseGraph_materialize line 301
  36. def OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.overlay line 318

    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.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.Table

  37. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.overlay_rotation_old line 323
  38. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.overlay_rotation_expander line 330
  39. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.overlay_accepts_old line 337
  40. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.overlay_accepts_expander line 344
  41. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.overlay_semantics line 350
  42. def OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.lazy line 358
  43. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.lazy_rotation_false line 361
  44. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.lazy_rotation_true line 367
  45. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.lazy_accepts_false line 374
  46. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.lazy_accepts_true line 380
  47. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.lazy_semantics line 387
  48. theorem OAI.MaxCutGames.Foundations.PCP.CloudRounding.dart_rejection_count_le line 406
  49. def OAI.MaxCutGames.Foundations.PCP.CloudRounding.colorSet line 455
  50. def OAI.MaxCutGames.Foundations.PCP.CloudRounding.minoritySet line 458
  51. def OAI.MaxCutGames.Foundations.PCP.CloudRounding.directedCut line 461
  52. def OAI.MaxCutGames.Foundations.PCP.CloudRounding.disagreementSet line 464
  53. abbrev OAI.MaxCutGames.Foundations.PCP.CloudRounding.Nonmajor line 467
  54. theorem OAI.MaxCutGames.Foundations.PCP.CloudRounding.exists_max_color line 470
  55. def OAI.MaxCutGames.Foundations.PCP.CloudRounding.majority line 477
  56. theorem OAI.MaxCutGames.Foundations.PCP.CloudRounding.majority_maximal line 481
  57. theorem OAI.MaxCutGames.Foundations.PCP.CloudRounding.nonchosen_color_twice_le line 487

    Source documentation

    Every nonchosen color occupies at most half the cloud.

    theorem nonchosen_color_twice_le (ell : X → A) (m : A)
    (maximal : ∀ a, (colorSet ell a).card ≤ (colorSet ell m).card)
    (a : A) (ha : a ≠ m) :
    2 * (colorSet ell a).card ≤ Fintype.card X := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.CloudRounding.colorSet

  58. def OAI.MaxCutGames.Foundations.PCP.CloudRounding.minorityEquiv line 506
  59. theorem OAI.MaxCutGames.Foundations.PCP.CloudRounding.minority_card_eq_sum line 523
  60. def OAI.MaxCutGames.Foundations.PCP.CloudRounding.minorityCutEmbedding line 529

    Source documentation

    The tail label determines the forgotten minority color.

    def minorityCutEmbedding (ell : X → A) (next : X × D → X) (m : A) :
    (Σ a : Nonmajor m, ↥(directedCut next (colorSet ell a.val))) ↪
      ↥(disagreementSet ell next) where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.CloudRounding.Nonmajor, OAI.MaxCutGames.Foundations.PCP.CloudRounding.directedCut, OAI.MaxCutGames.Foundations.PCP.CloudRounding.colorSet, OAI.MaxCutGames.Foundations.PCP.CloudRounding.disagreementSet

  61. theorem OAI.MaxCutGames.Foundations.PCP.CloudRounding.minority_cut_sum_le line 555
  62. theorem OAI.MaxCutGames.Foundations.PCP.CloudRounding.minority_expansion_bound line 563

    Source documentation

    Sum genuine directed-cut expansion over the nonchosen color classes.

    theorem minority_expansion_bound (ell : X → A) (next : X × D → X) (m : A)
    (h : ℚ)
    (maximal : ∀ a, (colorSet ell a).card ≤ (colorSet ell m).card)
    (expansion : ∀ S : Finset X, S.card ≤ Fintype.card X / 2 →
      h * (S.card : ℚ) ≤ ((directedCut next S).card : ℚ)) :
    h * ((minoritySet ell m).card : ℚ) ≤ ((disagreementSet ell next).card : ℚ) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.CloudRounding.colorSet, OAI.MaxCutGames.Foundations.PCP.CloudRounding.directedCut, OAI.MaxCutGames.Foundations.PCP.CloudRounding.minoritySet, OAI.MaxCutGames.Foundations.PCP.CloudRounding.disagreementSet

  63. def OAI.MaxCutGames.Foundations.PCP.CloudRounding.mismatchSet line 593
  64. def OAI.MaxCutGames.Foundations.PCP.CloudRounding.copiedRejectionCount line 597
  65. def OAI.MaxCutGames.Foundations.PCP.CloudRounding.innerDisagreementSet line 600
  66. def OAI.MaxCutGames.Foundations.PCP.CloudRounding.roundLabels line 604
  67. def OAI.MaxCutGames.Foundations.PCP.CloudRounding.mismatchFiberEquiv line 609

    Source documentation

    Every changed dart belongs to precisely one tail fiber.

    def mismatchFiberEquiv (G : ConstraintGraph V E A) (ell : E → A)
    (rounded : V → A) :
    (Σ v, ↥(minoritySet (fun e : Cloud G v => ell e.val) (rounded v))) ≃
      ↥(mismatchSet G ell rounded) where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.CloudRounding.minoritySet, OAI.MaxCutGames.Foundations.PCP.CloudRounding.mismatchSet

  68. theorem OAI.MaxCutGames.Foundations.PCP.CloudRounding.mismatch_card_eq_sum line 627
  69. def OAI.MaxCutGames.Foundations.PCP.CloudRounding.disagreementFiberEquiv line 635

    Source documentation

    A cloud disagreement is the same actual internal dart in global coordinates.

    def disagreementFiberEquiv (G : ConstraintGraph V E A)
    (H : ∀ v, PortGraph (Cloud G v) D) (ell : E → A) :
    (Σ v, ↥(disagreementSet (fun e : Cloud G v => ell e.val)
      (fun ed => ((H v).rot ed).1))) ≃ ↥(innerDisagreementSet G H ell) where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.CloudRounding.disagreementSet, OAI.MaxCutGames.Foundations.PCP.CloudRounding.innerDisagreementSet

  70. theorem OAI.MaxCutGames.Foundations.PCP.CloudRounding.disagreement_card_eq_sum line 657
  71. theorem OAI.MaxCutGames.Foundations.PCP.CloudRounding.rounded_mismatch_expansion line 666

    Source documentation

    No uniform cloud-size hypothesis occurs in this finite sum.

    theorem rounded_mismatch_expansion [Nonempty A]
    (G : ConstraintGraph V E A) (H : ∀ v, PortGraph (Cloud G v) D)
    (ell : E → A) (h : ℚ)
    (expansion : ∀ v (S : Finset (Cloud G v)),
      S.card ≤ Fintype.card (Cloud G v) / 2 →
      h * (S.card : ℚ) ≤ ((directedCut (fun ed => ((H v).rot ed).1) S).card : ℚ)) :
    h * ((mismatchSet G ell (roundLabels G ell)).card : ℚ) ≤
      ((innerDisagreementSet G H ell).card : ℚ) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.CloudRounding.directedCut, OAI.MaxCutGames.Foundations.PCP.CloudRounding.mismatchSet, OAI.MaxCutGames.Foundations.PCP.CloudRounding.roundLabels, OAI.MaxCutGames.Foundations.PCP.CloudRounding.innerDisagreementSet

  72. theorem OAI.MaxCutGames.Foundations.PCP.CloudRounding.rounded_endpoint_bound line 683
  73. theorem OAI.MaxCutGames.Foundations.PCP.CloudRounding.copied_satisfied_inl line 690
  74. theorem OAI.MaxCutGames.Foundations.PCP.CloudRounding.copied_satisfied_inr line 696
  75. theorem OAI.MaxCutGames.Foundations.PCP.CloudRounding.replacement_rejection_split line 703

    Source documentation

    Exact rejection count for arbitrary copied labels, including cloud violations.

    theorem replacement_rejection_split (G : ConstraintGraph V E A)
    (H : ∀ v, PortGraph (Cloud G v) D) (ell : E → A) :
    (replacementGraph G H).rejectionCount ell =
      copiedRejectionCount G ell + (innerDisagreementSet G H ell).card := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.CloudRounding.copiedRejectionCount, OAI.MaxCutGames.Foundations.PCP.CloudRounding.innerDisagreementSet

  76. theorem OAI.MaxCutGames.Foundations.PCP.CloudRounding.replacement_soundness line 716

    Source documentation

    Directed expansion by two pays for both changed endpoints exactly.

    theorem replacement_soundness [Nonempty A]
    (G : ConstraintGraph V E A) (H : ∀ v, PortGraph (Cloud G v) D)
    (expansion : ∀ v (S : Finset (Cloud G v)),
      S.card ≤ Fintype.card (Cloud G v) / 2 →
      2 * S.card ≤ (directedCut (fun ed => ((H v).rot ed).1) S).card)
    (ell : E → A) :
    G.rejectionCount (roundLabels G ell) ≤ (replacementGraph G H).rejectionCount ell := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.CloudRounding.directedCut, OAI.MaxCutGames.Foundations.PCP.CloudRounding.roundLabels

  77. theorem OAI.MaxCutGames.Foundations.PCP.CloudRounding.padded_replacement_soundness line 733

    Source documentation

    Padding changes the normalization, but never the rounded absolute rejection count.

    theorem padded_replacement_soundness [Nonempty A]
    (G : ConstraintGraph V E A) (dummy : V → Type*) [∀ v, Fintype (dummy v)]
    [∀ v, DecidableEq (dummy v)]
    (H : ∀ v, PortGraph (Cloud (paddedGraph G dummy) v) D)
    (expansion : ∀ v (S : Finset (Cloud (paddedGraph G dummy) v)),
      S.card ≤ Fintype.card (Cloud (paddedGraph G dummy) v) / 2 →
      2 * S.card ≤ (directedCut (fun ed => ((H v).rot ed).1) S).card)
    (ell : PaddedDart G dummy → A) :
    G.rejectionCount (roundLabels (paddedGraph G dummy) ell) ≤
      (paddedReplacementGraph G dummy H).rejectionCount ell := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.CloudRounding.directedCut, OAI.MaxCutGames.Foundations.PCP.CloudRounding.roundLabels

  78. theorem OAI.MaxCutGames.Foundations.PCP.CloudRounding.combine_counts line 749

    Source documentation

    The exact coefficient obtained by combining endpoint charging and expansion.

    theorem combine_counts (R b M c : Nat) (h : ℚ) (hh : 0 < h)
    (endpoint : R ≤ b + 2 * M) (cloud : h * (M : ℚ) ≤ (c : ℚ)) :
    (R : ℚ) ≤ max 1 (2 / h) * ((b : ℚ) + (c : ℚ)) := by
…