OAI/Computability/UniqueGames/PCP/CloudRoundingLemmas.lean

GitHub source file

62 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. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.dart_rejection_count_le line 25
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.colorSet line 74
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.minoritySet line 77
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.directedCut line 80
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.disagreementSet line 83
  6. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.Nonmajor line 86
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.exists_max_color line 89
  8. def OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.majority line 96
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.majority_maximal line 100
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.nonchosen_color_twice_le line 106

    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.UniqueGamesTheorem.Foundations.PCP.CloudRounding.colorSet

  11. def OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.minorityEquiv line 125
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.minority_card_eq_sum line 142
  13. def OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.minorityCutEmbedding line 148

    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.UniqueGamesTheorem.Foundations.PCP.CloudRounding.Nonmajor, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.directedCut, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.colorSet, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.disagreementSet

  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.minority_cut_sum_le line 174
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.minority_expansion_bound line 182

    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.UniqueGamesTheorem.Foundations.PCP.CloudRounding.colorSet, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.directedCut, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.minoritySet, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.disagreementSet

  16. def OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.mismatchSet line 212
  17. def OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.copiedRejectionCount line 216
  18. def OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.innerDisagreementSet line 219
  19. def OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.roundLabels line 223
  20. def OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.mismatchFiberEquiv line 228

    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.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.minoritySet, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.mismatchSet

  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.mismatch_card_eq_sum line 246
  22. def OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.disagreementFiberEquiv line 254

    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.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.disagreementSet, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.innerDisagreementSet

  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.disagreement_card_eq_sum line 276
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.rounded_mismatch_expansion line 285

    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.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.directedCut, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.mismatchSet, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.roundLabels, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.innerDisagreementSet

  25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.rounded_endpoint_bound line 302
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.copied_satisfied_inl line 309
  27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.copied_satisfied_inr line 315
  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.replacement_rejection_split line 322

    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.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.copiedRejectionCount, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.innerDisagreementSet

  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.replacement_soundness line 335

    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.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.directedCut, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.roundLabels

  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.padded_replacement_soundness line 352

    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.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.directedCut, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.roundLabels

  31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.combine_counts line 368

    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
…
  32. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Label line 409
  33. def OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.rowIndex line 411
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.rowIndex_val line 414
  35. structure OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table line 418

    Source documentation

    Finite executable input data, with the two graph laws certified on lookup.

    structure Table (vertices ports : Nat) where
…
  36. def OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.rotation line 430

    Source documentation

    One reverse-index lookup and the fixed mixed-radix decoding.

    def rotation (table : Table n d) (e : Fin n × Fin d) : Fin n × Fin d :=
…

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

  37. def OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.accepts line 434

    Source documentation

    Lookup of the full stored binary predicate.

    def accepts (table : Table n d) (e : Fin n × Fin d) (a b : Label) : Bool :=
…

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

  38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.rowIndex_rotation line 437
  39. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.rotation_involutive line 441
  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.accepts_rotation line 447
  41. def OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.portGraph line 452

    Source documentation

    The actual reversible regular port graph represented by the vectors.

    def portGraph (table : Table n d) : PortGraph (Fin n) (Fin d) where
…

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

  42. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.portGraph_rot line 460
  43. def OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.baseGraph line 464

    Source documentation

    Constraint-graph semantics, with each vertex-port pair a distinct dart.

    def baseGraph (table : Table n d) : ConstraintGraph (Fin n) (Fin n × Fin d) Label where
…

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

  44. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.baseGraph_reverse line 471
  45. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.baseGraph_tail line 474
  46. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.baseGraph_head line 477
  47. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.baseGraph_accepts line 480
  48. def OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.ofPortGraph line 484

    Source documentation

    Materialize a reversible port graph and its predicates into the fixed rows.

    def ofPortGraph (G : PortGraph (Fin n) (Fin d))
    (predicate : (Fin n × Fin d) → Label → Label → Bool)
    (htranspose : ∀ e a b, predicate (G.rot e) b a = predicate e a b) : Table n d where
…

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

  49. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.rotation_ofPortGraph line 501
  50. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.accepts_ofPortGraph line 508
  51. def OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.flatRows line 516
  52. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.reverseAt_flatRows line 520
  53. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.acceptsAt_flatRows line 524
  54. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.flatRows_valid line 528
  55. def OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.graphTable line 535
  56. def OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.tableWords line 539

    Source documentation

    Existing graph codec, with header [n,n*d] and 4098 words in every row.

    def tableWords (table : Table n d) : List Nat := GraphTables.tableWords (graphTable table)

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.tableWords, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.graphTable

  57. def OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.tableBits line 541
  58. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Input line 544

    Source documentation

    Variable vertex count, with the port count fixed by the input family.

    abbrev Input (ports : Nat) := (vertices : Nat) × Table vertices ports

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

  59. def OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.inputBits line 546
  60. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.tableWords_eq line 548
  61. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.tableWords_length line 551
  62. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.vertices_le_tableBits_length line 555