Stretched edges: the independent sets of a graph, read off a bipartite one

The combinatorial core of the reduction from counting the independent sets of a graph to counting those of a bipartite graph. Replace every edge u – v by t paths u – w – v through new middle vertices: the result is bipartite, the vertices on one side and the middles on the other. An independent set of it is any set S of vertices together with any set of middles of the edges having no endpoint in S (DescriptiveComplexity.bisIndep_stretch_iff), so there are

∑ S, (2 ^ t) ^ e(S)

of them, e(S) being the number of edges with no endpoint in S. When 2 ^ t exceeds the number 2 ^ n of sets of vertices, the remainder modulo 2 ^ t is the number of sets S with e(S) = 0, i.e., whose complement is independent (DescriptiveComplexity.card_bisIndep_stretch_mod).

@[reducible, inline]

abbrev DescriptiveComplexity.EdgePair {V : Type} (Adj : V → V → Prop) : Type

The edges of a graph, as ordered pairs of distinct adjacent vertices.

Equations

• DescriptiveComplexity.EdgePair Adj = { p : V × V // p.1 ≠ p.2 ∧ Adj p.1 p.2 }

def DescriptiveComplexity.StretchIndep {V W : Type} (Adj : V → V → Prop) (T : V ⊕ EdgePair Adj × W → Prop) : Prop

Independence in the stretched graph: no chosen middle vertex has a chosen endpoint.

Equations

• DescriptiveComplexity.StretchIndep Adj T = ∀ (q : DescriptiveComplexity.EdgePair Adj × W) (a : V), T (Sum.inr q) → T (Sum.inl a) → ¬(a = (↑q.1).1 ∨ a = (↑q.1).2)

theorem DescriptiveComplexity.card_stretchIndep_mod {V W : Type} [Finite V] [Finite W] (Adj : V → V → Prop) (hW : Nat.card V < Nat.card W) : Nat.card { T : V ⊕ EdgePair Adj × W → Prop // StretchIndep Adj T } % 2 ^ Nat.card W = Nat.card { U : V → Prop // IndepSet Adj U }

The independent sets of a graph, as a remainder. In the graph whose edges are stretched through |W| middle vertices each, W having more elements than the graph has vertices, the number of independent sets modulo 2 ^ |W| is the number of independent sets of the graph.