Constraint graphs and their unsatisfiability value

A constraint graph Dinur, Section 2.1 over an alphabet α is a multigraph with finitely many edges, each of which carries a binary constraint on the labels of its two ends. A labelling σ : V → α of the vertices violates the edges whose constraints its labels fail, and the unsatisfiability value unsatVal is the least fraction of edges that a labelling violates. It vanishes exactly on the satisfiable constraint graphs, and Dinur's proof of the PCP theorem amplifies it: every step of the proof is a transformation of constraint graphs that keeps satisfiable graphs satisfiable and multiplies the value of unsatisfiable ones by at least a constant factor.

Vertices and edges are types rather than numbers: the constructions of the proof (degree reduction, expanderization, powering) produce vertices and edges that are pairs, sums or tuples of those of their inputs. Edges are indexed, so parallel edges and self-loops are allowed, and directed, from src e to dst e, so that a constraint need not be symmetric; an undirected edge is modelled by its two orientations when the construction needs it. The fractions are taken over the edges only, so the vertex type need not be finite. A constraint graph without edges has value zero, as is right: it is satisfied by every labelling.

Main definitions

• Cslib.PCP.ConstraintGraph: a multigraph with a binary constraint on each edge.
• Cslib.PCP.ConstraintGraph.Satisfies, Cslib.PCP.ConstraintGraph.Satisfiable.
• Cslib.PCP.ConstraintGraph.unsatEdges, Cslib.PCP.ConstraintGraph.unsatFrac: the edges a labelling violates, and their proportion.
• Cslib.PCP.ConstraintGraph.unsatVal: the least proportion of violated edges.
• Cslib.PCP.ConstraintGraph.map: the vertices renamed, for instance to add isolated vertices.
• Cslib.PCP.ConstraintGraph.comap: the edges pulled back along a map, for instance renamed.
• Cslib.PCP.ConstraintGraph.reindex: the vertices and the edges renamed along equivalences.
• Cslib.PCP.ConstraintGraph.union: two constraint graphs on the same vertices, superposed.

Main results

• Cslib.PCP.ConstraintGraph.expect_mem_unsatEdges: the proportion of violated edges is the probability that a uniformly random edge is violated.
• Cslib.PCP.ConstraintGraph.exists_unsatFrac_eq_unsatVal: the minimum is attained.
• Cslib.PCP.ConstraintGraph.unsatVal_eq_zero_iff: the value vanishes exactly on satisfiable constraint graphs.
• Cslib.PCP.ConstraintGraph.inv_card_le_unsatVal, Cslib.PCP.ConstraintGraph.one_le_card_mul_unsatVal: an unsatisfiable constraint graph has value at least one edge's worth.
• Cslib.PCP.ConstraintGraph.unsatVal_map: renaming the vertices injectively preserves the value.
• Cslib.PCP.ConstraintGraph.satisfiable_comap_iff, Cslib.PCP.ConstraintGraph.unsatVal_comap_equiv: pulling back along a surjection preserves satisfiability, and along an equivalence the value.
• Cslib.PCP.ConstraintGraph.satisfiable_reindex_iff, Cslib.PCP.ConstraintGraph.unsatVal_reindex: renaming the vertices and the edges preserves satisfiability and the value.
• Cslib.PCP.ConstraintGraph.card_mul_unsatVal_add_le, Cslib.PCP.ConstraintGraph.card_mul_unsatVal_le_union: adding edges can only increase the number of edges violated by the best labelling.
• Cslib.PCP.ConstraintGraph.unsatVal_union_of_forall_rel: adding edges whose constraints always hold scales the value by the proportion of the original edges.

References

• I. Dinur, The PCP theorem by gap amplification
• I. Dinur, The PCP theorem by gap amplification, ECCC TR05-046, revision 1
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

structure Cslib.PCP.ConstraintGraph (V : Type u_1) (E : Type u_2) (α : Type u_3) : Type (max (max u_1 u_2) u_3)

A constraint graph Dinur, Section 2.1 on the vertices V, with edges indexed by E, over the alphabet α: each edge e goes from src e to dst e and carries a binary constraint rel e on the labels of its ends. Parallel edges and self-loops are allowed.

• src : E → V

  The first end of an edge.

• dst : E → V

  The second end of an edge.

• rel : E → α → α → Prop

  The constraint on an edge: a relation between the labels of its first and second ends.

theorem Cslib.PCP.ConstraintGraph.ext_iff {V : Type u_1} {E : Type u_2} {α : Type u_3} {x y : ConstraintGraph V E α} : x = y ↔ x.src = y.src ∧ x.dst = y.dst ∧ x.rel = y.rel

theorem Cslib.PCP.ConstraintGraph.ext {V : Type u_1} {E : Type u_2} {α : Type u_3} {x y : ConstraintGraph V E α} (src : x.src = y.src) (dst : x.dst = y.dst) (rel : x.rel = y.rel) : x = y

def Cslib.PCP.ConstraintGraph.Satisfies {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) (σ : V → α) (e : E) : Prop

The labelling σ satisfies the edge e when the labels of its ends satisfy its constraint.

def Cslib.PCP.ConstraintGraph.Satisfiable {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) : Prop

A constraint graph is satisfiable when some labelling satisfies all of its edges.

noncomputable def Cslib.PCP.ConstraintGraph.unsatEdges {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] (σ : V → α) : Finset E

The edges that the labelling σ violates.

@[simp]

theorem Cslib.PCP.ConstraintGraph.mem_unsatEdges {V : Type u_1} {E : Type u_2} {α : Type u_4} {G : ConstraintGraph V E α} [Fintype E] {σ : V → α} {e : E} : e ∈ G.unsatEdges σ ↔ ¬G.Satisfies σ e

theorem Cslib.PCP.ConstraintGraph.unsatEdges_eq_empty_iff {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] {σ : V → α} : G.unsatEdges σ = ∅ ↔ ∀ (e : E), G.Satisfies σ e

A labelling violates no edge exactly when it satisfies all of them.

theorem Cslib.PCP.ConstraintGraph.card_unsatEdges_le {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] (σ : V → α) : (G.unsatEdges σ).card ≤ Fintype.card E

A labelling violates at most all the edges.

noncomputable def Cslib.PCP.ConstraintGraph.unsatFrac {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] (σ : V → α) : ℝ

The proportion of the edges that the labelling σ violates, UNSAT_σ(G) in Dinur, Section 2.1. It is zero when there are no edges.

theorem Cslib.PCP.ConstraintGraph.card_mul_unsatFrac {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] (σ : V → α) : ↑(Fintype.card E) * G.unsatFrac σ = ↑(G.unsatEdges σ).card

The number of violated edges is the proportion of violated edges times the number of edges.

theorem Cslib.PCP.ConstraintGraph.unsatFrac_nonneg {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] (σ : V → α) : 0 ≤ G.unsatFrac σ

The proportion of violated edges is nonnegative.

theorem Cslib.PCP.ConstraintGraph.unsatFrac_le_one {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] (σ : V → α) : G.unsatFrac σ ≤ 1

The proportion of violated edges is at most one.

theorem Cslib.PCP.ConstraintGraph.unsatFrac_eq_zero_iff {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] {σ : V → α} : G.unsatFrac σ = 0 ↔ ∀ (e : E), G.Satisfies σ e

A labelling violates no proportion of the edges exactly when it satisfies all of them.

theorem Cslib.PCP.ConstraintGraph.expect_mem_unsatEdges {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] [DecidableEq E] (σ : V → α) : (Finset.univ.expect fun (e : E) => if e ∈ G.unsatEdges σ then 1 else 0) = G.unsatFrac σ

The proportion of the edges that a labelling violates is the average of the indicator of the violated edges: the probability that it violates a uniformly random edge.

noncomputable def Cslib.PCP.ConstraintGraph.unsatVal {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] : ℝ

The unsatisfiability value UNSAT(G) Dinur, Section 2.1: the least proportion of the edges that a labelling violates. The minimum is attained when α is nonempty (exists_unsatFrac_eq_unsatVal); when there is no labelling at all, the value is zero by convention.

theorem Cslib.PCP.ConstraintGraph.bddBelow_range_unsatFrac {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] : BddBelow (Set.range G.unsatFrac)

The proportions of violated edges are bounded below, by zero.

theorem Cslib.PCP.ConstraintGraph.unsatVal_le {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] (σ : V → α) : G.unsatVal ≤ G.unsatFrac σ

The value is at most the proportion of the edges that any labelling violates.

theorem Cslib.PCP.ConstraintGraph.unsatVal_nonneg {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] : 0 ≤ G.unsatVal

The value is nonnegative.

theorem Cslib.PCP.ConstraintGraph.unsatVal_le_one {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] : G.unsatVal ≤ 1

The value is at most one.

theorem Cslib.PCP.ConstraintGraph.unsatVal_of_isEmpty {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] [IsEmpty E] : G.unsatVal = 0

A constraint graph without edges has value zero.

theorem Cslib.PCP.ConstraintGraph.finite_range_unsatFrac {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] : (Set.range G.unsatFrac).Finite

The proportion of violated edges takes finitely many values, multiples of 1 / |E|.

theorem Cslib.PCP.ConstraintGraph.exists_unsatFrac_eq_unsatVal {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] [Nonempty α] : ∃ (σ : V → α), G.unsatFrac σ = G.unsatVal

The minimum is attained: some labelling violates exactly the proportion unsatVal of the edges.

theorem Cslib.PCP.ConstraintGraph.le_unsatVal_iff {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] [Nonempty α] {c : ℝ} : c ≤ G.unsatVal ↔ ∀ (σ : V → α), c ≤ G.unsatFrac σ

A lower bound on the value is a lower bound on the proportion of the edges violated by every labelling.

theorem Cslib.PCP.ConstraintGraph.unsatVal_le_iff {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] [Nonempty α] {c : ℝ} : G.unsatVal ≤ c ↔ ∃ (σ : V → α), G.unsatFrac σ ≤ c

An upper bound on the value is an upper bound on the proportion of the edges violated by some labelling.

theorem Cslib.PCP.ConstraintGraph.unsatVal_eq_zero_iff {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] [Nonempty α] : G.unsatVal = 0 ↔ G.Satisfiable

The value vanishes exactly on satisfiable constraint graphs.

theorem Cslib.PCP.ConstraintGraph.unsatVal_pos_iff {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] [Nonempty α] : 0 < G.unsatVal ↔ ¬G.Satisfiable

The value is positive exactly on unsatisfiable constraint graphs.

theorem Cslib.PCP.ConstraintGraph.inv_card_le_unsatVal {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] [Nonempty α] (h : ¬G.Satisfiable) : (↑(Fintype.card E))⁻¹ ≤ G.unsatVal

An unsatisfiable constraint graph has value at least 1 / |E|: every labelling violates at least one edge.

theorem Cslib.PCP.ConstraintGraph.one_le_card_mul_unsatVal {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] [Nonempty α] (h : ¬G.Satisfiable) : 1 ≤ ↑(Fintype.card E) * G.unsatVal

An unsatisfiable constraint graph violates at least one edge at its minimum-value labelling.

def Cslib.PCP.ConstraintGraph.map {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) {W : Type u_5} (f : V → W) : ConstraintGraph W E α

The constraint graph G with its vertices renamed along f : V → W: the same edges and constraints, between the images of their ends. The vertices outside the range of f are isolated.

@[simp]

theorem Cslib.PCP.ConstraintGraph.satisfies_map {V : Type u_1} {E : Type u_2} {α : Type u_4} {G : ConstraintGraph V E α} {W : Type u_5} {f : V → W} {τ : W → α} {e : E} : (G.map f).Satisfies τ e ↔ G.Satisfies (τ ∘ f) e

A labelling satisfies an edge of G.map f when its composite with f satisfies it in G.

theorem Cslib.PCP.ConstraintGraph.satisfiable_map {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) {W : Type u_5} [Nonempty α] {f : V → W} (hf : Function.Injective f) : (G.map f).Satisfiable ↔ G.Satisfiable

Renaming the vertices injectively preserves satisfiability.

theorem Cslib.PCP.ConstraintGraph.unsatEdges_map {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) {W : Type u_5} (f : V → W) [Fintype E] (τ : W → α) : (G.map f).unsatEdges τ = G.unsatEdges (τ ∘ f)

A labelling violates the edges of G.map f that its composite with f violates in G.

theorem Cslib.PCP.ConstraintGraph.unsatFrac_map {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) {W : Type u_5} (f : V → W) [Fintype E] (τ : W → α) : (G.map f).unsatFrac τ = G.unsatFrac (τ ∘ f)

A labelling violates the same proportion of the edges of G.map f as its composite with f does of the edges of G.

theorem Cslib.PCP.ConstraintGraph.unsatVal_le_unsatVal_map {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) {W : Type u_5} (f : V → W) [Fintype E] [Nonempty α] : G.unsatVal ≤ (G.map f).unsatVal

Renaming the vertices can only increase the value: the labellings of the renamed constraint graph give labellings of the original one.

theorem Cslib.PCP.ConstraintGraph.unsatVal_map {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) {W : Type u_5} [Fintype E] [Nonempty α] {f : V → W} (hf : Function.Injective f) : (G.map f).unsatVal = G.unsatVal

Renaming the vertices injectively preserves the value: for instance, adding isolated vertices does not change it.

def Cslib.PCP.ConstraintGraph.comap {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) (g : F → E) : ConstraintGraph V F α

The constraint graph G pulled back along a map g : F → E of edges: its edge f is a copy of the edge g f of G, with the same ends and the same constraint. Renaming the edges along an equivalence, repeating them or keeping only some of them are pullbacks.

@[simp]

theorem Cslib.PCP.ConstraintGraph.satisfies_comap {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} {G : ConstraintGraph V E α} {g : F → E} {σ : V → α} {f : F} : (G.comap g).Satisfies σ f ↔ G.Satisfies σ (g f)

A labelling satisfies an edge of G.comap g when it satisfies its image in G.

@[simp]

theorem Cslib.PCP.ConstraintGraph.comap_id {V : Type u_1} {E : Type u_2} {α : Type u_4} (G : ConstraintGraph V E α) : G.comap id = G

Pulling back along the identity does nothing.

theorem Cslib.PCP.ConstraintGraph.comap_comap {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) {F' : Type u_5} (g : F → E) (h : F' → F) : (G.comap g).comap h = G.comap (g ∘ h)

Pulling back twice is pulling back along the composite.

theorem Cslib.PCP.ConstraintGraph.Satisfiable.comap {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} {G : ConstraintGraph V E α} (h : G.Satisfiable) (g : F → E) : (G.comap g).Satisfiable

A labelling satisfying G satisfies its pullbacks.

theorem Cslib.PCP.ConstraintGraph.satisfiable_comap_iff {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) {g : F → E} (hg : Function.Surjective g) : (G.comap g).Satisfiable ↔ G.Satisfiable

Pulling back along a surjective map of edges preserves satisfiability.

theorem Cslib.PCP.ConstraintGraph.mem_unsatEdges_comap {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) (g : F → E) [Fintype E] [Fintype F] {σ : V → α} {f : F} : f ∈ (G.comap g).unsatEdges σ ↔ g f ∈ G.unsatEdges σ

A labelling violates the edges of G.comap g whose images it violates in G.

theorem Cslib.PCP.ConstraintGraph.unsatEdges_comap_equiv {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] [Fintype F] (e : F ≃ E) (σ : V → α) : (G.comap ⇑e).unsatEdges σ = Finset.map e.symm.toEmbedding (G.unsatEdges σ)

Renaming the edges along an equivalence renames the violated edges.

theorem Cslib.PCP.ConstraintGraph.card_unsatEdges_comap_equiv {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] [Fintype F] (e : F ≃ E) (σ : V → α) : ((G.comap ⇑e).unsatEdges σ).card = (G.unsatEdges σ).card

Renaming the edges along an equivalence preserves the number of violated edges.

theorem Cslib.PCP.ConstraintGraph.unsatFrac_comap_equiv {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] [Fintype F] (e : F ≃ E) (σ : V → α) : (G.comap ⇑e).unsatFrac σ = G.unsatFrac σ

Renaming the edges along an equivalence preserves the proportion of violated edges.

theorem Cslib.PCP.ConstraintGraph.unsatVal_comap_equiv {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) [Fintype E] [Fintype F] (e : F ≃ E) : (G.comap ⇑e).unsatVal = G.unsatVal

Renaming the edges along an equivalence preserves the value.

def Cslib.PCP.ConstraintGraph.reindex {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) {W : Type u_5} (eV : V ≃ W) (eE : E ≃ F) : ConstraintGraph W F α

The constraint graph G with its vertices and its edges renamed along equivalences: for instance numbered by Fin (Fintype.equivFin).

@[simp]

theorem Cslib.PCP.ConstraintGraph.satisfies_reindex {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} {G : ConstraintGraph V E α} {W : Type u_5} {eV : V ≃ W} {eE : E ≃ F} {τ : W → α} {f : F} : (G.reindex eV eE).Satisfies τ f ↔ G.Satisfies (τ ∘ ⇑eV) (eE.symm f)

A labelling satisfies an edge of the renamed constraint graph when its composite with the renaming of the vertices satisfies the corresponding edge of G.

theorem Cslib.PCP.ConstraintGraph.satisfiable_reindex_iff {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) {W : Type u_5} (eV : V ≃ W) (eE : E ≃ F) : (G.reindex eV eE).Satisfiable ↔ G.Satisfiable

Renaming the vertices and the edges preserves satisfiability.

theorem Cslib.PCP.ConstraintGraph.unsatVal_reindex {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) {W : Type u_5} [Fintype E] [Fintype F] (eV : V ≃ W) (eE : E ≃ F) : (G.reindex eV eE).unsatVal = G.unsatVal

Renaming the vertices and the edges preserves the value.

def Cslib.PCP.ConstraintGraph.union {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) (H : ConstraintGraph V F α) : ConstraintGraph V (E ⊕ F) α

The union of two constraint graphs on the same vertices: its edges are those of G, labelled by Sum.inl, and those of H, labelled by Sum.inr, with their constraints.

@[simp]

theorem Cslib.PCP.ConstraintGraph.satisfies_union_inl {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} {G : ConstraintGraph V E α} {H : ConstraintGraph V F α} {σ : V → α} {e : E} : (G.union H).Satisfies σ (Sum.inl e) ↔ G.Satisfies σ e

@[simp]

theorem Cslib.PCP.ConstraintGraph.satisfies_union_inr {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} {G : ConstraintGraph V E α} {H : ConstraintGraph V F α} {σ : V → α} {f : F} : (G.union H).Satisfies σ (Sum.inr f) ↔ H.Satisfies σ f

theorem Cslib.PCP.ConstraintGraph.satisfiable_union_iff {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) (H : ConstraintGraph V F α) : (G.union H).Satisfiable ↔ ∃ (σ : V → α), (∀ (e : E), G.Satisfies σ e) ∧ ∀ (f : F), H.Satisfies σ f

The union is satisfied by the labellings that satisfy both constraint graphs.

theorem Cslib.PCP.ConstraintGraph.card_unsatEdges_union {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) (H : ConstraintGraph V F α) [Fintype E] [Fintype F] (σ : V → α) : ((G.union H).unsatEdges σ).card = (G.unsatEdges σ).card + (H.unsatEdges σ).card

A labelling violates the edges of the union that it violates in either constraint graph.

theorem Cslib.PCP.ConstraintGraph.card_add_card_mul_unsatFrac_union {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) (H : ConstraintGraph V F α) [Fintype E] [Fintype F] (σ : V → α) : (↑(Fintype.card E) + ↑(Fintype.card F)) * (G.union H).unsatFrac σ = ↑(Fintype.card E) * G.unsatFrac σ + ↑(Fintype.card F) * H.unsatFrac σ

The proportion of the edges of the union that a labelling violates is the average of those in the two constraint graphs, weighted by their numbers of edges.

theorem Cslib.PCP.ConstraintGraph.card_mul_unsatVal_add_le {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) (H : ConstraintGraph V F α) [Fintype E] [Fintype F] [Nonempty α] : ↑(Fintype.card E) * G.unsatVal + ↑(Fintype.card F) * H.unsatVal ≤ (↑(Fintype.card E) + ↑(Fintype.card F)) * (G.union H).unsatVal

The value of a union: the best labelling of the union violates at least as many edges as the best labellings of the two constraint graphs together.

theorem Cslib.PCP.ConstraintGraph.card_mul_unsatVal_le_union {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) (H : ConstraintGraph V F α) [Fintype E] [Fintype F] [Nonempty α] : ↑(Fintype.card E) * G.unsatVal ≤ (↑(Fintype.card E) + ↑(Fintype.card F)) * (G.union H).unsatVal

Adding edges to a constraint graph can only increase the number of edges violated by the best labelling.

theorem Cslib.PCP.ConstraintGraph.unsatFrac_union_of_forall_rel {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) (H : ConstraintGraph V F α) [Fintype E] [Fintype F] (hH : ∀ (f : F) (a b : α), H.rel f a b) (σ : V → α) : (G.union H).unsatFrac σ = ↑(Fintype.card E) / (↑(Fintype.card E) + ↑(Fintype.card F)) * G.unsatFrac σ

Adding edges whose constraints always hold scales the proportion of violated edges by the proportion of the original edges.

theorem Cslib.PCP.ConstraintGraph.unsatVal_union_of_forall_rel {V : Type u_1} {E : Type u_2} {F : Type u_3} {α : Type u_4} (G : ConstraintGraph V E α) (H : ConstraintGraph V F α) [Fintype E] [Fintype F] (hH : ∀ (f : F) (a b : α), H.rel f a b) : (G.union H).unsatVal = ↑(Fintype.card E) / (↑(Fintype.card E) + ↑(Fintype.card F)) * G.unsatVal

Adding edges whose constraints always hold scales the value by the proportion of the original edges.