OAI/Computability/MaxCut/PCP/PreprocessingRegularTables.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

Executable degree replacement on the actual finite constraint rows

Vertices are numbered by first listing the original darts, then the dummy darts in original-vertex order. Each local cloud uses its explicit filtered dart list. Internal ports carry equality; the final port retains the original constraint, or an always-accepting loop at a dummy dart. The constructor is total, including inputs with no darts. The fixed base expander is supplied once; every input-dependent operation is an explicit finite calculation.

  1. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.paddingList line 23

    Source documentation

    Dummy coordinates, in increasing original vertex and local index order.

    def paddingList {n : Nat} (padding : Fin n → Nat) :
    List (Σ v : Fin n, Fin (padding v)) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.padding

  2. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.paddingList_nodup line 27
  3. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.mem_paddingList line 31
  4. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.paddingListOrder line 36
  5. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.paddingList_length line 41
  6. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.paddingOrder line 47

    Source documentation

    Explicit list search/get indexing, with an erased cardinality cast.

    def paddingOrder {n : Nat} (padding : Fin n → Nat) :
    (Σ v : Fin n, Fin (padding v)) ≃ Fin (∑ v, padding v) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.padding

  7. abbrev OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.Vertex line 51
  8. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.vertexCount line 54
  9. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder line 58

    Source documentation

    The original darts precede all the newly added dummy darts.

    def vertexOrder (t : GraphTables.Table) (padding : Fin t.vertices → Nat) :
    Vertex t padding ≃ Fin (vertexCount t padding) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.padding, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.Vertex, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.vertexCount

  10. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder_original line 62
  11. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder_dummy line 66
  12. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.unitOrder line 71
  13. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.portOrder line 78

    Source documentation

    Internal cloud ports precede the one inherited-constraint port.

    def portOrder (q : Nat) : (Fin q ⊕ Unit) ≃ Fin (q + 1) :=
…
  14. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.portOrder_internal line 81
  15. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.portOrder_inherited line 84
  16. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.cloudGraphs line 88

    Source documentation

    A supplied finite cloud rotation is transported by the explicit cloud list.

    def cloudGraphs (t : GraphTables.Table) (padding : Fin t.vertices → Nat)
    {q : Nat} (tables : ∀ v, ExpanderTables.Table
      (PreprocessingCloudIndex.cloudSize t v + padding v) q) (v : Fin t.vertices) :
    PortGraph (Cloud (paddedGraph (GraphTables.semantics t)
      (fun w => Fin (padding w))) v) (Fin q) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.padding, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.Table, OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize, OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics

  17. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.sourcePortGraph line 96
  18. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.sourceGraph line 103
  19. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.numberedPortGraph line 111
  20. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.numberedAccepts line 118
  21. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.numberedAccepts_transpose line 126
  22. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.ofCloudTables line 140

    Source documentation

    Materialize every reverse index and every 4096-bit constraint row.

    def ofCloudTables (t : GraphTables.Table) (padding : Fin t.vertices → Nat)
    {q : Nat} (tables : ∀ v, ExpanderTables.Table
      (PreprocessingCloudIndex.cloudSize t v + padding v) q) :
    PortTables.Table (vertexCount t padding) (q + 1) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.padding, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.Table, OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize, OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.vertexCount

  23. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.rotation_ofCloudTables line 147
  24. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.accepts_ofCloudTables line 159
  25. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.accepts_internal line 170
  26. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.accepts_original line 180
  27. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.accepts_dummy line 191
  28. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.edgeSatisfied_ofCloudTables line 201
  29. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.rejectionCount_ofCloudTables line 219

    Source documentation

    Numbering preserves the rejection count for every labeling.

    theorem rejectionCount_ofCloudTables (t : GraphTables.Table)
    (padding : Fin t.vertices → Nat) {q : Nat}
    (tables : ∀ v, ExpanderTables.Table
      (PreprocessingCloudIndex.cloudSize t v + padding v) q)
    (labels : Fin (vertexCount t padding) → GraphTables.Label) :
    (PortTables.baseGraph (ofCloudTables t padding tables)).rejectionCount labels =
      (sourceGraph t padding tables).rejectionCount
        (fun z => labels (vertexOrder t padding z)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.padding, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.Table, OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.vertexCount, OAI.MaxCutGames.Foundations.PCP.GraphTables.Label, OAI.MaxCutGames.Foundations.PCP.PortTables.baseGraph, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.ofCloudTables, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.sourceGraph, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder

  30. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.liftedLabel line 235
  31. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.rejectionCount_liftedLabel line 241
  32. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.emptyTable line 254

    Source documentation

    An empty cloud has a total, vacuous rotation table.

    def emptyTable (q : Nat) : ExpanderTables.Table 0 q :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ExpanderTables.Table

  33. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.resizeTable line 258

    Source documentation

    Change only a proof-equal size index, without selecting any new numbering.

    def resizeTable {n m q : Nat} (h : n = m) (table : ExpanderTables.Table n q) :
    ExpanderTables.Table m q := h ▸ table

    Mentions: OAI.MaxCutGames.Foundations.PCP.ExpanderTables.Table

  34. abbrev OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.BaseTable line 261
  35. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.internalDegree line 265
  36. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.padding line 267
  37. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.cloudSize_add_padding line 271
  38. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_eq_sum_cloudPaddedSize line 276
  39. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_le line 283
  40. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_eq_zero_of_no_darts line 289
  41. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.familyCloudTable line 296

    Source documentation

    Select the family level by the bounded multiplication search.

    def familyCloudTable (H : BaseTable) (t : GraphTables.Table) (v : Fin t.vertices) :
    ExpanderTables.Table (PreprocessingCloudIndex.cloudSize t v + padding t v)
      internalDegree :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.BaseTable, OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.Table, OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.padding, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.internalDegree

  42. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.regularize line 310

    Source documentation

    The actual regularized output rows; no runtime proof or positivity input.

    def regularize (H : BaseTable) (t : GraphTables.Table) :
    PortTables.Table (vertexCount t (padding t)) (internalDegree + 1) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.BaseTable, OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.vertexCount, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.padding, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.internalDegree

  43. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularTables.regularizeInput line 314
  44. def OAI.MaxCutGames.Foundations.PCP.VertexPadding.reverseFunction line 327

    Source documentation

    Original darts use the original reversal; dummy darts stay fixed.

    def reverseFunction (G : ConstraintGraph V (V × D) A) (extra : ℕ) :
    (V ⊕ Fin extra) × D → (V ⊕ Fin extra) × D
  | (Sum.inl v, d) => (Sum.inl (G.reverse (v, d)).1, (G.reverse (v, d)).2)
  | (Sum.inr w, d) => (Sum.inr w, d)

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph

  45. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.reverseFunction_involutive line 332
  46. def OAI.MaxCutGames.Foundations.PCP.VertexPadding.pad line 341

    Source documentation

    Actual regular padding by an arbitrary finite number of dummy vertices.

    def pad (G : ConstraintGraph V (V × D) A) (extra : ℕ) :
    ConstraintGraph (V ⊕ Fin extra) ((V ⊕ Fin extra) × D) A where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph

  47. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.pad_tail line 359
  48. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.pad_reverse_inl line 362
  49. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.pad_reverse_inr line 367
  50. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.edgeSatisfied_inl line 371
  51. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.edgeSatisfied_inr line 382
  52. def OAI.MaxCutGames.Foundations.PCP.VertexPadding.extendLabeling line 386
  53. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.extendLabeling_inl line 389
  54. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.extendLabeling_inr line 392
  55. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.pad_satisfiable line 395
  56. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.satisfiable_of_pad line 403
  57. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.rejectionCount_eq_sum_inline_VertexPadding line 410
  58. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.pad_rejectionCount line 416

    Source documentation

    Exact counts for every padded labeling, without any condition on dummy labels.

    theorem pad_rejectionCount [Fintype V] [Fintype D]
    (G : ConstraintGraph V (V × D) A) (htail : G.tail = Prod.fst) (extra : ℕ)
    (labeling : V ⊕ Fin extra → A) :
    (pad G extra).rejectionCount labeling =
      G.rejectionCount (fun v => labeling (Sum.inl v)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.VertexPadding.pad

  59. def OAI.MaxCutGames.Foundations.PCP.VertexPadding.extraVertices line 428
  60. abbrev OAI.MaxCutGames.Foundations.PCP.VertexPadding.Vertex line 430
  61. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.card_vertex line 432
  62. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.le_card_vertex line 436
  63. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.card_vertex_le line 440
  64. def OAI.MaxCutGames.Foundations.PCP.VertexPadding.familyVertexEquiv line 446

    Source documentation

    Exact coordinate bridge to the proved geometric family.

    noncomputable def familyVertexEquiv :
    Vertex V ≃ ExpanderFamily.Vertex (ExpanderFamily.level (Fintype.card V)) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.VertexPadding.Vertex, OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.Vertex, OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.level

  65. def OAI.MaxCutGames.Foundations.PCP.VertexPadding.paddedG line 454
  66. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.paddedG_tail line 457
  67. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.paddedG_rejectionCount line 460
  68. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.rejectionCount_eq line 467
  69. def OAI.MaxCutGames.Foundations.PCP.VertexPadding.liftLabel line 474
  70. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.liftLabel_inl line 477
  71. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.liftLabel_inr line 480
  72. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.rejectionCount_liftLabel line 484
  73. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.paddedG_satisfiable line 491
  74. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.card_padded_darts line 495
  75. theorem OAI.MaxCutGames.Foundations.PCP.VertexPadding.card_padded_darts_le line 499
  76. def OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv line 525

    Source documentation

    Old vertices occupy the initial interval and dummy vertices the final one.

    def vertexEquiv (h : n ≤ m) : Fin n ⊕ Fin (m - n) ≃ Fin m :=
…
  77. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_inl line 528
  78. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_inr_val line 531
  79. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_symm_old line 534
  80. def OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.dartEquiv line 539

    Source documentation

    The port number is retained by the coordinate conversion.

    def dartEquiv (h : n ≤ m) :
    (Fin n ⊕ Fin (m - n)) × Fin d ≃ Fin m × Fin d :=
…
  81. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.dartEquiv_apply line 543
  82. def OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.sumGraph line 548

    Source documentation

    Concrete sum-type padding, before converting to integer vertex indices.

    def sumGraph (table : Table n d) (m : Nat) :
    ConstraintGraph (Fin n ⊕ Fin (m - n))
      ((Fin n ⊕ Fin (m - n)) × Fin d) Label :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph

  83. def OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph line 554

    Source documentation

    The same graph, with the explicit initial/final-interval vertex ordering.

    def paddedGraph (table : Table n d) (h : n ≤ m) :
    ConstraintGraph (Fin m) (Fin m × Fin d) Label where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph

  84. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_reverse_equiv line 571
  85. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_accepts_equiv line 579
  86. def OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.pad line 587

    Source documentation

    Executable materialization of every padded rotation and predicate row.

    def pad (table : Table n d) (h : n ≤ m) : Table m d :=
…
  87. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad line 593
  88. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad line 597
  89. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.pad_valid line 603

    Source documentation

    These are the actual finite table validity laws, not additional premises.

    theorem pad_valid (table : Table n d) (h : n ≤ m) :
    Function.Involutive (rotation (pad table h)) ∧
      ∀ e a b, PortTables.accepts (pad table h) (rotation (pad table h) e) b a =
        PortTables.accepts (pad table h) e a b :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.pad, OAI.MaxCutGames.Foundations.PCP.PortTables.accepts

  90. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.constraintGraph_ext_inline_PreprocessingPaddingTables line 609
  91. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.baseGraph_pad line 624

    Source documentation

    Full semantic identity with the concrete padding and explicit reindexing.

    @[simp] theorem baseGraph_pad (table : Table n d) (h : n ≤ m) :
    baseGraph (pad table h) = paddedGraph table h := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.pad, OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph

  92. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_equiv line 632
  93. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_old line 640
  94. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_new line 647
  95. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad_old line 654
  96. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad_new line 660
  97. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.reverseIndex_pad_old line 666
  98. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.reverseIndex_pad_new line 672
  99. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.relation_ext_inline_PreprocessingPaddingTables line 678
  100. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.relations_pad_old line 688

    Source documentation

    The entire old 4096-bit relation row is retained.

    theorem relations_pad_old (table : Table n d) (h : n ≤ m)
    (v : Fin n) (p : Fin d) :
    (pad table h).relations[rowIndex m d (v.castLE h, p)] =
      table.relations[rowIndex n d (v, p)] := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.pad

  101. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.relations_pad_new line 697

    Source documentation

    Every bit of every added relation row PortTables.accepts.

    theorem relations_pad_new (table : Table n d) (h : n ≤ m)
    (v : Fin (m - n)) (p : Fin d) :
    (pad table h).relations[rowIndex m d (vertexEquiv h (Sum.inr v), p)] =
      Vector.replicate 4096 true := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.pad, OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv

  102. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_edgeSatisfied_equiv line 708

    Source documentation

    Pointwise satisfaction commutes with the explicit sum-coordinate map.

    theorem paddedGraph_edgeSatisfied_equiv (table : Table n d) (h : n ≤ m)
    (labeling : Fin m → Label) (e : (Fin n ⊕ Fin (m - n)) × Fin d) :
    (paddedGraph table h).edgeSatisfied labeling (dartEquiv h e) =
      (sumGraph table m).edgeSatisfied (fun v => labeling (vertexEquiv h v)) e := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph, OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.dartEquiv, OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.sumGraph, OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv

  103. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_equiv line 720
  104. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_old line 727
  105. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_new line 735
  106. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.pad_rejectionCount line 742

    Source documentation

    Exact occurrence counts for arbitrary labels on all old and added vertices.

    theorem pad_rejectionCount (table : Table n d) (h : n ≤ m)
    (labeling : Fin m → Label) :
    (baseGraph (pad table h)).rejectionCount labeling =
      (baseGraph table).rejectionCount (fun v => labeling (v.castLE h)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.pad

  107. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.pad_labeling_satisfies_iff line 761

    Source documentation

    A particular padded labeling satisfies exactly when its old restriction does.

    theorem pad_labeling_satisfies_iff (table : Table n d) (h : n ≤ m)
    (labeling : Fin m → Label) :
    (∀ e, (baseGraph (pad table h)).edgeSatisfied labeling e = true) ↔
      ∀ e, (baseGraph table).edgeSatisfied (fun v => labeling (v.castLE h)) e = true := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.pad

  108. def OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.extendLabeling line 777

    Source documentation

    A computable extension uses label zero on every dummy vertex.

    def extendLabeling (h : n ≤ m) (labeling : Fin n → Label) : Fin m → Label :=
…
  109. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.extendLabeling_old line 780
  110. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingPaddingTables.pad_satisfiable_iff line 784