Pendant leaves: the independent sets of one size, read off a digit

The combinatorial core of the reduction from counting the independent sets of a given size to counting all of them. Attach to every vertex of a graph on n vertices n new vertices, its leaves, adjacent to it alone (DescriptiveComplexity.pendAdj). An independent set of the new graph is an independent set S of the old one together with any set of leaves of the vertices outside S (DescriptiveComplexity.indepSet_pend_iff), so there are

∑ S, (2 ^ n) ^ (n - |S|)

of them, S ranging over the independent sets of the old graph. Fewer than 2 ^ n sets have each size (n being positive), so this is a number in base 2 ^ n whose digit of rank n - k is the number of independent sets of size k (DescriptiveComplexity.card_indepSet_pend_digit).

def DescriptiveComplexity.IndepSet {T : Type} (Adj : T → T → Prop) (S : T → Prop) : Prop

The set S is independent for Adj: no two distinct elements of it are related.

Equations

• DescriptiveComplexity.IndepSet Adj S = ∀ (x y : T), S x → S y → x ≠ y → ¬Adj x y

def DescriptiveComplexity.pendAdj {V : Type} (Adj : V → V → Prop) : V ⊕ V × V → V ⊕ V × V → Prop

Adjacency of the graph with pendant leaves: the vertices are those of V with the adjacency they had, and a leaf (a, i) is adjacent to a alone.

Equations

• DescriptiveComplexity.pendAdj Adj (Sum.inl a) (Sum.inl b) = Adj a b
• DescriptiveComplexity.pendAdj Adj (Sum.inl a) (Sum.inr p) = (a = p.1)
• DescriptiveComplexity.pendAdj Adj (Sum.inr p) (Sum.inl b) = (p.1 = b)
• DescriptiveComplexity.pendAdj Adj (Sum.inr val) (Sum.inr val_1) = False

theorem DescriptiveComplexity.indepSet_pend_iff {V : Type} (Adj : V → V → Prop) (T : V ⊕ V × V → Prop) : IndepSet (pendAdj Adj) T ↔ (IndepSet Adj fun (a : V) => T (Sum.inl a)) ∧ ∀ (p : V × V), T (Sum.inr p) → ¬T (Sum.inl p.1)

An independent set of the graph with leaves is an independent set of the graph, and leaves of vertices outside it.

theorem DescriptiveComplexity.card_indepSet_pend_digit {V : Type} [Finite V] [Nonempty V] (Adj : V → V → Prop) (Kp : V → Prop) : Nat.card { T : V ⊕ V × V → Prop // IndepSet (pendAdj Adj) T } / 2 ^ (Nat.card V * Nat.card { v : V // ¬Kp v }) % 2 ^ Nat.card V = Nat.card { S : V → Prop // IndepSet Adj S ∧ {x : V | S x}.ncard = {x : V | Kp x}.ncard }

The independent sets of one size, as a digit. In a graph on n ≥ 1 vertices with n leaves at every vertex, the number of independent sets, divided by (2 ^ n) ^ (n - k) and reduced modulo 2 ^ n, is the number of independent sets of size k of the graph; here k is the size of a set Kp, and n - k the number of elements outside it.