OAI/Computability/UniqueGames/PCP/PoweringPortReindexLemmas.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Exact transport of powering through a change of ports. The target's actual address selector is pulled back, so no compatibility of enumeration orders or consistency restriction on raw padded labels is needed.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.wordEquiv line 21
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.walkEquiv line 27
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.addressEquiv line 30
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.labelEquiv line 37

    Source documentation

    Pull target raw labels back to old port coordinates; this is a bijection.

    def labelEquiv (ports : D ≃ E) (t : Nat) : PaddedLabel E t A ≃ PaddedLabel D t A where
…
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.wordEnd_map line 49
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.endpoint_map line 57
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.reach_iff line 61
  8. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.ballEquiv line 72
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.wordToBall_map line 78
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.pullSelector line 85

    Source documentation

    Use the target selector, including its concrete enumeration choices.

    def pullSelector {t : Nat} {v : V} (S : AddressSelector H t v) :
    AddressSelector G t v where
…
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.decode_pullSelector line 93
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.decode_transport line 99
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.opinionAt_pullSelector line 109
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.advanceTail_map line 122
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.edgeAt_map line 130
  16. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.pullAccepts line 145
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.pathAccepts_map line 148
  18. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.dartEquiv line 174
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.edgeSatisfied_map line 177
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.rejectionCount_map line 190
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.satisfiable_iff line 211
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.pullReverse line 228
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.base_edgeSatisfied_map line 234
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.base_rejectionCount_map line 244
  25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.uniform_count_gap line 273

    Source documentation

    The generic lazy-graph gap survives a genuine rotation-preserving port change and the target's chosen selectors, for every raw target labeling.

    theorem uniform_count_gap
    [Fintype V] [Fintype D] [Fintype E] [Nonempty V] [Nonempty D]
    [Fintype A] [Nonempty A]
    (G : PortGraph V D) (H : PortGraph V E) (ports : (Bool × D) ≃ E)
    (rotation : ∀ v d, H.rot (v, ports d) =
      (((lazyGraph G).rot (v,d)).1, ports ((lazyGraph G).rot (v,d)).2))
    (lambda : ℝ) (certificate : SpectralCertificate (lazyGraph G) lambda)
    (accepts : Edge V E → A → A → Bool)
    (reverse_accepts : ∀ e a b, accepts (H.rot e) b a = accepts e a b)
    (M : Nat) (hM : 1 ≤ M)
    (selectors : ∀v, AddressSelector H (2*center (Fintype.card A) M+1) v)
    (epsilon : ℝ) (hepsilon : 0 ≤ epsilon)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.accepts

  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.lazy_table_uniform_count_gap line 313

    Source documentation

    Gap bound for the actual numbered power table built from a lazified port table. The spectral certificate is on the genuine Boolean-flag lazy graph.

    theorem lazy_table_uniform_count_gap {vertices d : Nat}
    (input : PortTables.Table vertices d) (hv : 0 < vertices) (hd : 0 < d)
    (lambda : ℝ)
    (certificate : SpectralCertificate (lazyGraph (PortTables.portGraph input)) lambda)
    (M : Nat) (hM : 1 ≤ M) (epsilon : ℝ) (hepsilon : 0 ≤ epsilon)
    (hgap : ∀ assignment : Fin vertices → Fin 64,
      epsilon * (Fintype.card (Fin vertices × Fin (2*d)) : ℝ) ≤
        ((PortTables.baseGraph (PreprocessingOverlayTables.lazy input)).rejectionCount assignment : ℝ)) :
    ∀ labels : PoweringTableSemantics.EncodedLabeling vertices (2*d) (2*center 64 M),
    (gain 64 M lambda * min epsilon (1 / ((2*center 64 M+1 : Nat) : ℝ))) *
      ((PoweringTables.table (PreprocessingOverlayTables.lazy input) (2*center 64 M)).darts : ℝ) ≤
      ((GenericGraphTables.semantics
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.portGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.baseGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.lazy, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.EncodedLabeling, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.table, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics

  27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringPortReindex.lazy_table_uniform_count_gap_at line 353

    Source documentation

    The same exact table bound with a separately stored walk parameter. Its proved equality may be used without evaluating a huge closed alphabet size.

    theorem lazy_table_uniform_count_gap_at {vertices d : Nat}
    (input : PortTables.Table vertices d) (hv : 0 < vertices) (hd : 0 < d)
    (lambda : ℝ)
    (certificate : SpectralCertificate (lazyGraph (PortTables.portGraph input)) lambda)
    (M : Nat) (hM : 1 ≤ M) (n : Nat) (hn : n = 2*center 64 M)
    (epsilon : ℝ) (hepsilon : 0 ≤ epsilon)
    (hgap : ∀ assignment : Fin vertices → Fin 64,
      epsilon * (Fintype.card (Fin vertices × Fin (2*d)) : ℝ) ≤
        ((PortTables.baseGraph (PreprocessingOverlayTables.lazy input)).rejectionCount
          assignment : ℝ)) :
    ∀ labels : PoweringTableSemantics.EncodedLabeling vertices (2*d) n,
    (gain 64 M lambda * min epsilon (1 / ((n+1 : Nat) : ℝ))) *
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.portGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.baseGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.lazy, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTableSemantics.EncodedLabeling

  28. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.Vertex line 397
  29. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.Port line 398
  30. def OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.degree line 401

    Source documentation

    The degree is one absolute constant, independent of the input graph.

    def degree : Nat := Fintype.card Port

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.Port

  31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.degree_eq line 403
  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.degree_positive line 406
  33. def OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.cloudEquiv line 409

    Source documentation

    A positive padded cloud has exactly the size of one explicit family member.

    def cloudEquiv (G : ConstraintGraph V E A) (v : V)
    (hk : 0 < Fintype.card (Cloud G v)) :
    ExpanderFamily.Vertex (ExpanderFamily.level (Fintype.card (Cloud G v))) ≃
      Cloud (paddedGraph G (CloudPadding.dummy G)) v :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.level, OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.dummy

  34. def OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.cloudGraph line 416

    Source documentation

    Empty clouds use the empty rotation; every other cloud uses the proved family.

    def cloudGraph (G : ConstraintGraph V E A) (v : V) :
    PortGraph (Cloud (paddedGraph G (CloudPadding.dummy G)) v) ExpanderFamily.Port :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.dummy, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.Port

  35. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.cloudGraph_of_pos line 427
  36. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.cloudGraph_certificate_of_pos line 435
  37. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.cloud_expansion line 444

    Source documentation

    The exact expansion premise required by the checked finite rounding theorem.

    theorem cloud_expansion (G : ConstraintGraph V E A) (v : V)
    (S : Finset (Cloud (paddedGraph G (CloudPadding.dummy G)) v))
    (hsmall : S.card ≤
      Fintype.card (Cloud (paddedGraph G (CloudPadding.dummy G)) v) / 2) :
    2 * S.card ≤
      (CloudRounding.directedCut (fun ed => ((cloudGraph G v).rot ed).1) S).card := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.CloudPadding.dummy, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.directedCut, OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.cloudGraph

  38. def OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.portGraph line 459
  39. def OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.graph line 463

    Source documentation

    The actual constraint graph, with its equality and inherited original tests.

    def graph (G : ConstraintGraph V E A) :
    ConstraintGraph (Vertex G) (Vertex G × Port) A :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.Port

  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.graph_tail line 468
  41. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.graph_reverse line 472
  42. def OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.degreeEquiv line 476

    Source documentation

    The outgoing darts at each new vertex are exactly its fixed port alphabet.

    def degreeEquiv (G : ConstraintGraph V E A) (v : Vertex G) :
    Cloud (graph G) v ≃ Port where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.graph, OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.Port

  43. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.fixed_degree line 488
  44. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.vertex_count_le line 493
  45. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.dart_count line 498
  46. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.dart_count_le line 503
  47. def OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.liftLabel line 513
  48. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.lift_rejectionCount line 518

    Source documentation

    Completeness preserves the absolute rejection count exactly.

    theorem lift_rejectionCount (G : ConstraintGraph V E A) (labeling : V → A) :
    (graph G).rejectionCount (liftLabel G labeling) = G.rejectionCount labeling :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.graph, OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.liftLabel

  49. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.completeness line 523
  50. def OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.roundLabels line 528
  51. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.soundness line 532

    Source documentation

    Actual regularization soundness with no remaining expansion or rounding premise.

    theorem soundness [Nonempty A] (G : ConstraintGraph V E A) (ell : Vertex G → A) :
    G.rejectionCount (roundLabels G ell) ≤ (graph G).rejectionCount ell :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.roundLabels, OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.graph

  52. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.exists_rounding line 537
  53. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.soundness_of_uniform_lower_bound line 541